defpred S₁[ Nat] means for S being finite Subset of K st S is simplex-like holds
card S <= $1;
assume A1: ( not K is void & K is finite-degree ) ; :: thesis:
then A2: the_family_of K is finite-membered by MATROID0:def 6;
A3: ex n being Nat st S₁[n] by A1;
consider k being Nat such that
A4: S₁[k] and
A5: for n being Nat st S₁[n] holds
k <= n from NAT_1:sch 5(A3);
take D = k - 1; :: thesis:
thus for S being finite Subset of K st S is simplex-like holds
card S <= D + 1 by A4; :: thesis:
assume A6: for S being Subset of K st S is simplex-like holds
card S <> D + 1 ; :: thesis:

suppose A7: k = 0 ; :: thesis:

consider S being object such that
A8: S in the topology of K by A1, XBOOLE_0:def 1;
reconsider S = S as finite Subset of K by A2, A8;
A9: S is simplex-like by A8;
then card S = 0 by A4, A7;
hence contradiction by A6, A7, A9; :: thesis:

end;

suppose k > 0 ; :: thesis:

then reconsider k1 = k - 1 as Element of NAT by NAT_1:20;
S₁[k1]

let S be finite Subset of K; :: thesis:
assume A10: S is simplex-like ; :: thesis:
then card S <= k1 + 1 by A4;
then card S < k1 + 1 by A6, A10, XXREAL_0:1;
hence card S <= k1 by NAT_1:13; :: thesis:

end;

then k1 + 1 <= k1 by A5;
hence contradiction by NAT_1:13; :: thesis:

end;

end;

end;

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