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 FINSET_1:def 6 :: 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;
then A3: X in the topology of K ;
the_family_of K is finite-membered by MATROID0:def 6;
hence x is finite by A3; :: thesis: verum