Existence of basic feasible solutions for bounded and standard-form polyhedra

For every real $m \times n$ matrix $A$ and $b \in \mathbb{R}^m$, the theorem asserts a conjunction of two implications. (a) If the "$\ge$"-form polyhedron $P = \{x \mid Ax \ge b\}$ is nonempty and bounded (some real $K$ bounds $|x_i| \le K$ for all $x \in P$ and coordinates $i$), then there exists a basic feasible solution $x$ of the general-form constraint system consisting of the $m$ constraints $A_i \cdot x \ge b_i$ — i.e. an $x$ satisfying all these constraints such that some $n$-element set of them is active at $x$ ($A_i \cdot x = b_i$) with linearly independent rows $(A_i)$; since this system has no "$=$"-tagged constraints, the equality clause of "basic" is vacuous, and existence of such an $x$ forces $m \ge n$. (b) If the standard-form polyhedron $\{x \mid Ax = b,\ x \ge 0\}$ is nonempty, then there exists a basic feasible solution of the standard-form system ($m$ equality constraints $A_i \cdot x = b_i$ plus $n$ sign constraints $x_j \ge 0$): all equalities active, all constraints satisfied, and some $n$ of the combined constraint vectors active at $x$ and linearly independent. No rank or independence hypothesis is placed on $A$ in either part.