let K be SimplicialComplexStr; :: thesis: ( K is locally-finite & K is subset-closed implies K is finite-membered )
assume A9: ( K is locally-finite & K is subset-closed ) ; :: thesis: K is finite-membered
the_family_of K is finite-membered

proof

let x be set ; :: according to MATROID0:def 5 :: thesis: ( not x in the_family_of K or x is finite )
assume A10: x in the_family_of K ; :: thesis: x is finite
then reconsider A = x as Subset of K ;
A11: not K is void by A10, PENCIL_1:def 4;
A12: A is simplex-like by A10, PRE_TOPC:def 2;

per cases ( x is empty or not x is empty ) ;

suppose x is empty ; :: thesis: x is finite

hence x is finite ; :: thesis: verum

end;

suppose not x is empty ; :: thesis: x is finite

then consider a being set such that
A13: a in A by XBOOLE_0:def 1;
reconsider a = a as Element of K by A13;
a is vertex-like by A12, A13, Def3;
then reconsider a = a as Vertex of K by Def4;
set Aa = A \ {a};
set X = { S where S is Subset of K : ( a in S & S c= A ) } ;
defpred S₁[ set , set ] means c₁ \ {a} = c₂;
set Z = { y where y is Element of bool (A \ {a}) : ex w being Subset of K st
( S₁[w,y] & w in { S where S is Subset of K : ( a in S & S c= A ) } ) } ;
A14: bool (A \ {a}) c= { y where y is Element of bool (A \ {a}) : ex w being Subset of K st
( S₁[w,y] & w in { S where S is Subset of K : ( a in S & S c= A ) } ) }

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in bool (A \ {a}) or y in { y where y is Element of bool (A \ {a}) : ex w being Subset of K st
( S₁[w,y] & w in { S where S is Subset of K : ( a in S & S c= A ) } ) } )
assume A15: y in bool (A \ {a}) ; :: thesis: y in { y where y is Element of bool (A \ {a}) : ex w being Subset of K st
( S₁[w,y] & w in { S where S is Subset of K : ( a in S & S c= A ) } ) }
then reconsider B = y as Subset of K by XBOOLE_1:1;
not a in B by A15, ZFMISC_1:56;
then A16: (B \/ {a}) \ {a} = B by ZFMISC_1:117;
A17: {a} c= A by A13, ZFMISC_1:31;
A \ {a} c= A by XBOOLE_1:36;
then y c= A by A15, XBOOLE_1:1;
then A18: B \/ {a} c= A by A17, XBOOLE_1:8;
then A19: B \/ {a} is Subset of K by XBOOLE_1:1;
a in {a} by TARSKI:def 1;
then a in B \/ {a} by XBOOLE_0:def 3;
then B \/ {a} in { S where S is Subset of K : ( a in S & S c= A ) } by A18, A19;
hence y in { y where y is Element of bool (A \ {a}) : ex w being Subset of K st
( S₁[w,y] & w in { S where S is Subset of K : ( a in S & S c= A ) } ) } by A15, A16, A19; :: thesis: verum

end;

set Y = { S where S is Subset of K : ( S is simplex-like & a in S ) } ;
A20: { S where S is Subset of K : ( a in S & S c= A ) } c= { S where S is Subset of K : ( S is simplex-like & a in S ) }

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { S where S is Subset of K : ( a in S & S c= A ) } or y in { S where S is Subset of K : ( S is simplex-like & a in S ) } )
assume y in { S where S is Subset of K : ( a in S & S c= A ) } ; :: thesis: y in { S where S is Subset of K : ( S is simplex-like & a in S ) }
then consider S being Subset of K such that
A21: ( y = S & a in S ) and
A22: S c= A ;
S is simplex-like by A9, A11, A12, A22, MATROID0:1;
hence y in { S where S is Subset of K : ( S is simplex-like & a in S ) } by A21; :: thesis: verum

end;

{ S where S is Subset of K : ( S is simplex-like & a in S ) } is finite by A9, Def6;
then A23: { S where S is Subset of K : ( a in S & S c= A ) } is finite by A20;
A24: for w being Subset of K
for x, y being Element of bool (A \ {a}) st S₁[w,x] & S₁[w,y] holds
x = y ;
{ y where y is Element of bool (A \ {a}) : ex w being Subset of K st
( S₁[w,y] & w in { S where S is Subset of K : ( a in S & S c= A ) } ) } is finite from FRAENKEL:sch 28(A23, A24);
then A25: A \ {a} is finite by A14;
A = (A \ {a}) \/ {a} by A13, ZFMISC_1:116;
hence x is finite by A25; :: thesis: verum

end;

end;

end;

hence K is finite-membered by MATROID0:def 6; :: thesis: verum