let S be SubSimplicialComplex of KX; :: thesis: S is finite-degree
consider n being Nat such that
A1: for A being finite Subset of KX st A is simplex-like holds
card A <= n by MATROID0:def 7;
thus S is finite-membered ; :: according to MATROID0:def 7 :: thesis: ex b₁ being set st
for b₂ being Element of bool the carrier of S holds
( not b₂ is simplex-like or card b₂ <= b₁ )
take n ; :: thesis: for b₁ being Element of bool the carrier of S holds
( not b₁ is simplex-like or card b₁ <= n )
let A be finite Subset of S; :: thesis: ( not A is simplex-like or card A <= n )
assume A is simplex-like ; :: thesis: card A <= n
then A2: A in the topology of S ;
[#] S c= [#] KX by Def13;
then reconsider A1 = A as finite Subset of KX by XBOOLE_1:1;
the topology of S c= the topology of KX by Def13;
then A1 is simplex-like by A2;
hence card A <= n by A1; :: thesis: verum