let K be SimplicialComplexStr; :: thesis: ( the topology of K is finite & not K is finite-vertices implies not K is finite-membered )
defpred S₁[ object , object ] means ex D2 being set st
( D2 = $2 & $1 in D2 );
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: Vertices K is infinite by A2;
A4: Vertices K = union the topology of K by Lm5;
A5: for x being object st x in Vertices K holds
ex y being object st
( y in the topology of K & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in Vertices K implies ex y being object st
( y in the topology of K & S₁[x,y] ) )
assume x in Vertices K ; :: thesis: ex y being object 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 object 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 object 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;
then dom f = Vertices K by FUNCT_2:def 1;
then consider x being object such that
A7: x in rng f and
A8: f " {x} is infinite by A1, A3, CARD_2:101;
x in the topology of K by A7;
then reconsider x = x as Subset of K ;
f " {x} c= x

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f " {x} or y in x )
assume A9: y in f " {x} ; :: thesis: y in x
then S₁[y,f . y] by A6;
then ( f . y in {x} & y in f . y ) by A9, 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;
hence not K is finite-membered ; :: thesis: verum