let S be Subset-Family of K; :: thesis: ( S is simplex-like implies S is finite-membered )
assume A1: S is simplex-like ; :: thesis: S is finite-membered
let x be set ; :: according to MATROID0:def 5 :: thesis: ( not x in S or x is finite )
assume A2: x in S ; :: thesis: x is finite
then reconsider X = x as Subset of K ;
X is simplex-like by A1, A2, TOPS_2:def 1;
then A3: X in the topology of K by PRE_TOPC:def 5;
the_family_of K is finite-membered by MATROID0:def 6;
hence x is finite by A3, MATROID0:def 5; :: thesis: verum