let K be SimplicialComplexStr; :: thesis: ( the topology of K is finite & not K is finite-vertices implies not K is finite-membered )
defpred S₁[ set , set ] means $1 in $2;
set V = Vertices K;
assume that
A1: the topology of K is finite and
A2: not K is finite-vertices ; :: thesis: not K is finite-membered
A3: not Vertices K is finite by A2, Def5;
A4: Vertices K = union the topology of K by Lm5;
A5: for x being set st x in Vertices K holds
ex y being set st
( y in the topology of K & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in Vertices K implies ex y being set st
( y in the topology of K & S₁[x,y] ) )
assume x in Vertices K ; :: thesis: ex y being set st
( y in the topology of K & S₁[x,y] )
then ex y being set st
( x in y & y in the topology of K ) by A4, TARSKI:def 4;
hence ex y being set st
( y in the topology of K & S₁[x,y] ) ; :: thesis: verum

end;

consider f being Function of (Vertices K), the topology of K such that
A6: for x being set st x in Vertices K holds
S₁[x,f . x] from FUNCT_2:sch 1(A5);
not the topology of K is empty by A2, A4, Def5;
then dom f = Vertices K by FUNCT_2:def 1;
then consider x being set such that
A7: x in rng f and
A8: not f " {x} is finite by A1, A3, COMPL_SP:24;
x in the topology of K by A7;
then reconsider x = x as Subset of K ;
f " {x} c= x

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in f " {x} or y in x )
assume y in f " {x} ; :: thesis: y in x
then ( f . y in {x} & y in f . y ) by A6, FUNCT_1:def 7;
hence y in x by TARSKI:def 1; :: thesis: verum

end;

then not x is finite by A8;
then not the_family_of K is finite-membered by A7, MATROID0:def 5;
hence not K is finite-membered by MATROID0:def 6; :: thesis: verum