let S be Simplex of - 1,K; :: thesis: S is empty
- 1 <= degree K by Th23;
then card S = (- 1) + 1 by Def18
.= 0 ;
hence S is empty ; :: thesis: verum