How to prove a linear program that is feasible and bounded is maximised at one of the basic feasible solution?
See for example the textbook Linear Programming by V. Chvatal. Chvatal proves this theorem constructively. The simplex method with an appropriate anti-cycling pivot selection rule (e.g. lexicographic or Bland's rule) terminates in one of three states (1) the LP has an optimal basic feasible solution (BFS), (2) the LP is unbounded, or (3) the LP is infeasible (this is detected in phase I.)