let i be Integer; :: thesis: for K being non void subset-closed SimplicialComplexStr st - 1 <= i & i <= degree K holds
ex S being Simplex of K st card S = i + 1
let K be non void subset-closed SimplicialComplexStr; :: thesis: ( - 1 <= i & i <= degree K implies ex S being Simplex of K st card S = i + 1 )
assume that
A1: - 1 <= i and
A2: i <= degree K ; :: thesis: ex S being Simplex of K st card S = i + 1
(- 1) + 1 <= i + 1 by A1, XREAL_1:6;
then reconsider i1 = i + 1 as Element of NAT by INT_1:3;

per cases ( not K is finite-degree or K is finite-degree ) ;

suppose A3: not K is finite-degree ; :: thesis: ex S being Simplex of K st card S = i + 1

per cases ( not K is finite-membered or for n being Nat ex A being finite Subset of K st
( A is open & card A > n ) ) by A3;

suppose not K is finite-membered ; :: thesis: ex S being Simplex of K st card S = i + 1

then not the_family_of K is finite-membered ;
then consider A being set such that
A4: A in the_family_of K and
A5: A is infinite ;
card i1 c= card A by A5;
then consider f being Function such that
A6: ( f is one-to-one & dom f = i1 ) and
A7: rng f c= A by CARD_1:10;
rng f in the_family_of K by A4, A7, CLASSES1:def 1;
then reconsider R = rng f as Simplex of K by PRE_TOPC:def 2;
take R ; :: thesis: card R = i + 1
R,i1 are_equipotent by A6, WELLORD2:def 4;
hence card R = i + 1 by CARD_1:def 2; :: thesis: verum

end;

suppose for n being Nat ex A being finite Subset of K st
( A is open & card A > n ) ; :: thesis: ex S being Simplex of K st card S = i + 1

then consider A being finite Subset of K such that
A8: A is simplex-like and
A9: card A > i1 ;
card (Segm i1) in card (Segm (card A)) by A9, NAT_1:41;
then card i1 c= card A by CARD_1:3;
then consider f being Function such that
A10: ( f is one-to-one & dom f = i1 ) and
A11: rng f c= A by CARD_1:10;
A in the_family_of K by A8;
then rng f in the_family_of K by A11, CLASSES1:def 1;
then reconsider R = rng f as Simplex of K by PRE_TOPC:def 2;
take R ; :: thesis: card R = i + 1
R,i1 are_equipotent by A10, WELLORD2:def 4;
hence card R = i + 1 by CARD_1:def 2; :: thesis: verum

end;

end;

end;

suppose A12: K is finite-degree ; :: thesis: ex S being Simplex of K st card S = i + 1

then reconsider d = degree K as Integer ;
consider S being Subset of K such that
A13: S is simplex-like and
A14: card S = (degree K) + 1 by A12, Def12;
reconsider s = S as finite Subset of K by A12, A13;
i + 1 <= d + 1 by A2, XREAL_1:6;
then Segm i1 c= Segm (card s) by A14, NAT_1:39;
then card i1 c= card (card s) ;
then consider f being Function such that
A15: ( f is one-to-one & dom f = i1 ) and
A16: rng f c= S by CARD_1:10;
S in the_family_of K by A13;
then rng f in the_family_of K by A16, CLASSES1:def 1;
then reconsider R = rng f as Simplex of K by PRE_TOPC:def 2;
take R ; :: thesis: card R = i + 1
R,i1 are_equipotent by A15, WELLORD2:def 4;
hence card R = i + 1 by CARD_1:def 2; :: thesis: verum

end;

end;