let D be non empty set ; :: thesis:
let K be non void subset-closed SimplicialComplexStr of D; :: thesis:
let S be non void SubSimplicialComplex of K; :: thesis:
let i be Integer; :: thesis:
let A be Simplex of i,S; :: thesis:
assume A1: ( not A is empty or i <= degree S or degree S = degree K ) ; :: thesis:
( A in the topology of S & the topology of S c= the topology of K ) by Def13, PRE_TOPC:def 2;
then A in the topology of K ;
then reconsider B = A as Simplex of K by PRE_TOPC:def 2;
A2: degree S <= degree K by Th32;

per cases by A1;

suppose A3: not A is empty ; :: thesis:

then A4: - 1 <= i by Def18;
A5: i <= degree S by A3, Def18;
- 1 <= i by A3, Def18;
then A6: card B = i + 1 by A5, Def18;
i <= degree K by A2, A5, XXREAL_0:2;
hence A is Simplex of i,K by A6, A4, Def18; :: thesis:

end;

suppose A7: i <= degree S ; :: thesis:

then A8: i <= degree K by A2, XXREAL_0:2;

per cases ;

suppose A9: - 1 <= i ; :: thesis:

then card B = i + 1 by A7, Def18;
hence A is Simplex of i,K by A8, A9, Def18; :: thesis:

end;

suppose A10: - 1 > i ; :: thesis:

then B is empty by Def18;
hence A is Simplex of i,K by A10, Def18; :: thesis:

end;

end;

end;

suppose A11: degree S = degree K ; :: thesis:

per cases ;

suppose A12: ( - 1 <= i & i <= degree S ) ; :: thesis:

then card B = i + 1 by Def18;
hence A is Simplex of i,K by A11, A12, Def18; :: thesis:

end;

suppose A13: ( - 1 > i or i > degree S ) ; :: thesis:

then B is empty by Def18;
hence A is Simplex of i,K by A11, A13, Def18; :: thesis:

end;

end;

end;

end;