per cases ( i < 0 or i >= 0 ) ;

suppose i < 0 ; :: thesis: ex b₁ being Simplex of max ((i - 1),(- 1)),K st b₁ c= S

then i - 1 < 0 - 1 by XREAL_1:8;
then reconsider F = the Simplex of - 1,K as Simplex of max ((i - 1),(- 1)),K by XXREAL_0:def 10;
take F ; :: thesis: F c= S
thus F c= S ; :: thesis: verum

end;

suppose A3: i >= 0 ; :: thesis: ex b₁ being Simplex of max ((i - 1),(- 1)),K st b₁ c= S

then A4: card S = i + 1 by A1, A2, Def18;
then not S is empty by A3;
then consider x being object such that
A5: x in S ;
reconsider I = i as Element of NAT by A1, A3, INT_1:3;
i - 1 <= (degree K) - 0 by A2, XXREAL_3:37;
then A6: i - 1 <= degree K by XXREAL_3:4;
reconsider Sx = S \ {x} as Simplex of K ;
A7: card Sx = (I - 1) + 1 by A4, A5, STIRL2_1:55;
A8: i - 1 >= 0 - 1 by A3, XREAL_1:6;
then max ((i - 1),(- 1)) = i - 1 by XXREAL_0:def 10;
then reconsider Sx = Sx as Simplex of max ((i - 1),(- 1)),K by A6, A7, A8, Def18;
take Sx ; :: thesis: Sx c= S
thus Sx c= S by XBOOLE_1:36; :: thesis: verum

end;

end;