A2: now :: thesis: ( ( - 1 > i or i > degree K ) implies ex S being Simplex of K st
( ( - 1 <= i & i <= degree K implies ex b₂ being finite Simplex of K st card b₂ = i + 1 ) & ( ( not - 1 <= i or not i <= degree K ) implies ex b₂ being finite Simplex of K st b₂ is empty ) ) )

reconsider S = {} K as Simplex of K ;
assume A3: ( - 1 > i or i > degree K ) ; :: thesis: ex S being Simplex of K st
( ( - 1 <= i & i <= degree K implies ex b₂ being finite Simplex of K st card b₂ = i + 1 ) & ( ( not - 1 <= i or not i <= degree K ) implies ex b₂ being finite Simplex of K st b₂ is empty ) )
take S = S; :: thesis: ( ( - 1 <= i & i <= degree K implies ex b₁ being finite Simplex of K st card b₁ = i + 1 ) & ( ( not - 1 <= i or not i <= degree K ) implies ex b₁ being finite Simplex of K st b₁ is empty ) )
S is empty ;
hence ( ( - 1 <= i & i <= degree K implies ex b₁ being finite Simplex of K st card b₁ = i + 1 ) & ( ( not - 1 <= i or not i <= degree K ) implies ex b₁ being finite Simplex of K st b₁ is empty ) ) by A3; :: thesis: verum

end;

now :: thesis: ( - 1 <= i & i <= degree K implies ex S being Simplex of K st
( ( - 1 <= i & i <= degree K implies ex b₂ being finite Simplex of K st card b₂ = i + 1 ) & ( ( not - 1 <= i or not i <= degree K ) implies ex b₂ being finite Simplex of K st b₂ is empty ) ) )

assume A4: ( - 1 <= i & i <= degree K ) ; :: thesis: ex S being Simplex of K st
( ( - 1 <= i & i <= degree K implies ex b₂ being finite Simplex of K st card b₂ = i + 1 ) & ( ( not - 1 <= i or not i <= degree K ) implies ex b₂ being finite Simplex of K st b₂ is empty ) )
then consider S being Simplex of K such that
A5: card S = i + 1 by A1, Lm7;
take S = S; :: thesis: ( ( - 1 <= i & i <= degree K implies ex b₁ being finite Simplex of K st card b₁ = i + 1 ) & ( ( not - 1 <= i or not i <= degree K ) implies ex b₁ being finite Simplex of K st b₁ is empty ) )
reconsider i = i as Integer by A1;
(- 1) + 1 <= i + 1 by A4, XXREAL_3:35;
then 0 <= i + 1 ;
then i + 1 in NAT by INT_1:3;
then S is finite by A5;
hence ( ( - 1 <= i & i <= degree K implies ex b₁ being finite Simplex of K st card b₁ = i + 1 ) & ( ( not - 1 <= i or not i <= degree K ) implies ex b₁ being finite Simplex of K st b₁ is empty ) ) by A4, A5; :: thesis: verum

end;

hence ( ( - 1 <= i & i <= degree K implies ex b₁ being finite Simplex of K st card b₁ = i + 1 ) & ( ( not - 1 <= i or not i <= degree K ) implies ex b₁ being finite Simplex of K st b₁ is empty ) ) by A2; :: thesis: verum