let K be SimplicialComplexStr; :: thesis: for S being finite Subset of K st S is simplex-like holds
card S <= (degree K) + 1
let S be finite Subset of K; :: thesis: ( S is simplex-like implies card S <= (degree K) + 1 )
assume A1: S is simplex-like ; :: thesis: card S <= (degree K) + 1
S in the topology of K by A1;
then A2: not K is void by PENCIL_1:def 4;

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

suppose K is finite-degree ; :: thesis: card S <= (degree K) + 1

hence card S <= (degree K) + 1 by A1, A2, Def12; :: thesis: verum

end;

suppose not K is finite-degree ; :: thesis: card S <= (degree K) + 1

then degree K = +infty by A2, Def12;
then (degree K) + 1 = +infty by XXREAL_3:def 2;
hence card S <= (degree K) + 1 by XXREAL_0:3; :: thesis: verum

end;

end;