let X be set ; :: thesis: for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX holds degree SX <= degree KX
let KX be SimplicialComplexStr of X; :: thesis: for SX being SubSimplicialComplex of KX holds degree SX <= degree KX
let SX be SubSimplicialComplex of KX; :: thesis: degree SX <= degree KX

per cases ( not SX is finite-degree or SX is void or ( not SX is void & SX is finite-degree ) ) ;

suppose A1: not SX is finite-degree ; :: thesis: degree SX <= degree KX

not SX is void

proof

assume SX is void ; :: thesis: contradiction
then SX is empty-membered ;
hence contradiction by A1; :: thesis: verum

end;

then ( not KX is finite-degree & not KX is void & degree SX = +infty ) by A1, Def12;
hence degree SX <= degree KX by Def12; :: thesis: verum

end;

suppose SX is void ; :: thesis: degree SX <= degree KX

then degree SX = - 1 by Def12;
hence degree SX <= degree KX by Th23; :: thesis: verum

end;

suppose A2: ( not SX is void & SX is finite-degree ) ; :: thesis: degree SX <= degree KX

then A3: not KX is void ;

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

suppose not KX is finite-degree ; :: thesis: degree SX <= degree KX

then degree KX = +infty by A3, Def12;
hence degree SX <= degree KX by XXREAL_0:3; :: thesis: verum

end;

suppose A4: KX is finite-degree ; :: thesis: degree SX <= degree KX

A5: the topology of SX c= the topology of KX by Def13;
consider S being Subset of SX such that
A6: S is simplex-like and
A7: card S = (degree SX) + 1 by A2, Def12;
A8: S in the topology of SX by A6, PRE_TOPC:def 2;
then S in the topology of KX by A5;
then reconsider S1 = S as finite Subset of KX by A4, A7;
S1 is simplex-like by A5, A8, PRE_TOPC:def 2;
then (degree SX) + 1 <= (degree KX) + 1 by A3, A4, A7, Def12;
then A9: ((degree SX) + 1) - 1 <= ((degree KX) + 1) - 1 by XXREAL_3:37;
((degree SX) + 1) - 1 = degree SX by XXREAL_3:24;
hence degree SX <= degree KX by A9, XXREAL_3:24; :: thesis: verum

end;

end;

end;

end;