let D1, D2 be ExtReal; :: thesis: ( ( not K is void & K is finite-degree & ( for S being finite Subset of K st S is simplex-like holds
card S <= D1 + 1 ) & ex S being Subset of K st
( S is simplex-like & card S = D1 + 1 ) & ( for S being finite Subset of K st S is simplex-like holds
card S <= D2 + 1 ) & ex S being Subset of K st
( S is simplex-like & card S = D2 + 1 ) implies D1 = D2 ) & ( K is void & D1 = - 1 & D2 = - 1 implies D1 = D2 ) & ( ( K is void or not K is finite-degree ) & not K is void & D1 = +infty & D2 = +infty implies D1 = D2 ) )

now :: thesis: ( not K is void & K is finite-degree & ( for S being finite Subset of K st S is simplex-like holds
card S <= D1 + 1 ) & ex S1 being Subset of K st
( S1 is simplex-like & card S1 = D1 + 1 ) & ( for S being finite Subset of K st S is simplex-like holds
card S <= D2 + 1 ) & ex S2 being Subset of K st
( S2 is simplex-like & card S2 = D2 + 1 ) implies D1 = D2 )

assume A11: ( not K is void & K is finite-degree ) ; :: thesis: ( ( for S being finite Subset of K st S is simplex-like holds
card S <= D1 + 1 ) & ex S1 being Subset of K st
( S1 is simplex-like & card S1 = D1 + 1 ) & ( for S being finite Subset of K st S is simplex-like holds
card S <= D2 + 1 ) & ex S2 being Subset of K st
( S2 is simplex-like & card S2 = D2 + 1 ) implies D1 = D2 )
assume A12: for S being finite Subset of K st S is simplex-like holds
card S <= D1 + 1 ; :: thesis: ( ex S1 being Subset of K st
( S1 is simplex-like & card S1 = D1 + 1 ) & ( for S being finite Subset of K st S is simplex-like holds
card S <= D2 + 1 ) & ex S2 being Subset of K st
( S2 is simplex-like & card S2 = D2 + 1 ) implies D1 = D2 )
given S1 being Subset of K such that A13: ( S1 is simplex-like & card S1 = D1 + 1 ) ; :: thesis: ( ( for S being finite Subset of K st S is simplex-like holds
card S <= D2 + 1 ) & ex S2 being Subset of K st
( S2 is simplex-like & card S2 = D2 + 1 ) implies D1 = D2 )
assume A14: for S being finite Subset of K st S is simplex-like holds
card S <= D2 + 1 ; :: thesis: ( ex S2 being Subset of K st
( S2 is simplex-like & card S2 = D2 + 1 ) implies D1 = D2 )
given S2 being Subset of K such that A15: ( S2 is simplex-like & card S2 = D2 + 1 ) ; :: thesis: D1 = D2
A16: D2 + 1 <= D1 + 1 by A11, A12, A15;
D1 + 1 <= D2 + 1 by A11, A13, A14;
hence D1 = D2 by A16, XXREAL_0:1, XXREAL_3:11; :: thesis: verum

end;

hence ( ( not K is void & K is finite-degree & ( for S being finite Subset of K st S is simplex-like holds
card S <= D1 + 1 ) & ex S being Subset of K st
( S is simplex-like & card S = D1 + 1 ) & ( for S being finite Subset of K st S is simplex-like holds
card S <= D2 + 1 ) & ex S being Subset of K st
( S is simplex-like & card S = D2 + 1 ) implies D1 = D2 ) & ( K is void & D1 = - 1 & D2 = - 1 implies D1 = D2 ) & ( ( K is void or not K is finite-degree ) & not K is void & D1 = +infty & D2 = +infty implies D1 = D2 ) ) ; :: thesis: verum