let K be SimplicialComplexStr; :: thesis: ( K is locally-finite & K is subset-closed implies K is finite-membered )
assume A8: ( 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 FINSET_1:def 6 :: thesis: ( not x in the_family_of K or x is finite )
assume A9: x in the_family_of K ; :: thesis: x is finite
then reconsider A = x as Subset of K ;
A10: not K is void by A9, PENCIL_1:def 4;
A11: A is simplex-like by A9;

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 object such that
A12: a in A ;
reconsider a = a as Element of K by A12;
a is vertex-like by A11, A12;
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 ) } ) } ;
A13: 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 object ; :: 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 A14: 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 A14, ZFMISC_1:56;
then A15: (B \/ {a}) \ {a} = B by ZFMISC_1:117;
A16: {a} c= A by A12, ZFMISC_1:31;
A \ {a} c= A by XBOOLE_1:36;
then B c= A by A14;
then A17: B \/ {a} c= A by A16, XBOOLE_1:8;
then A18: 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 A17, A18;
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 A14, A15, A18; :: thesis: verum

end;

set Y = { S where S is Subset of K : ( S is simplex-like & a in S ) } ;
A19: { 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 object ; :: 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
A20: ( y = S & a in S ) and
A21: S c= A ;
S is simplex-like by A8, A10, A11, A21, MATROID0:1;
hence y in { S where S is Subset of K : ( S is simplex-like & a in S ) } by A20; :: thesis: verum

end;

{ S where S is Subset of K : ( S is simplex-like & a in S ) } is finite by A8;
then A22: { S where S is Subset of K : ( a in S & S c= A ) } is finite by A19;
A23: 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(A22, A23);
then A24: A \ {a} is finite by A13;
A = (A \ {a}) \/ {a} by A12, ZFMISC_1:116;
hence x is finite by A24; :: thesis: verum

end;

end;

end;

hence K is finite-membered ; :: thesis: verum