let i be Integer; :: thesis:
let K be SimplicialComplexStr; :: thesis:
assume A1: ( not K is void or i >= - 1 ) ; :: thesis:

suppose A2: K is void ; :: thesis:

then A3: for S being finite Subset of K st S is simplex-like holds
card S <= i + 1 by PENCIL_1:def 4;
K is empty-membered by A2;
hence ( degree K <= i iff ( K is finite-membered & ( for S being finite Subset of K st S is simplex-like holds
card S <= i + 1 ) ) ) by A1, A2, A3, Th22; :: thesis:

end;

suppose A4: not K is void ; :: thesis:

hereby :: thesis:

assume A5: degree K <= i ; :: thesis:
then A6: (degree K) + 1 <= i + 1 by XXREAL_3:35;
i in REAL by XREAL_0:def 1;
then A7: degree K <> +infty by A5, XXREAL_0:9;
then ( K is finite-degree or K is empty-membered ) by Def12;
hence K is finite-membered ; :: thesis:
let S be finite Subset of K; :: thesis:
assume A8: S is simplex-like ; :: thesis:
( ( not K is void & K is finite-degree ) or K is void ) by A7, Def12;
then card S <= (degree K) + 1 by A4, A8, Def12;
hence card S <= i + 1 by A6, XXREAL_0:2; :: thesis:

end;

assume that
A9: K is finite-membered and
A10: for S being finite Subset of K st S is simplex-like holds
card S <= i + 1 ; :: thesis:
consider S being object such that
A11: S in the topology of K by A4, XBOOLE_0:def 1;
reconsider S = S as Subset of K by A11;
A12: S is simplex-like by A11;
then reconsider S = S as finite Subset of K by A9;
card S <= i + 1 by A10, A12;
then reconsider i1 = i + 1 as Element of NAT by INT_1:3;
for A being finite Subset of K st A is open holds
card A <= i1 by A10;
then A13: K is finite-degree by A9;
then reconsider d = degree K as Integer ;
ex S1 being Subset of K st
( S1 is simplex-like & card S1 = (degree K) + 1 ) by A4, A13, Def12;
then d + 1 <= i + 1 by A9, A10;
hence degree K <= i by XREAL_1:6; :: thesis:

end;

end;