let K be SimplicialComplexStr; :: thesis: ( K is finite-vertices implies ( K is locally-finite & K is finite-degree ) )
assume A5: K is finite-vertices ; :: thesis: ( K is locally-finite & K is finite-degree )
then reconsider V = Vertices K as finite Subset of K ;
thus K is locally-finite :: thesis: K is finite-degree

proof

let v be Vertex of K; :: according to SIMPLEX0:def 6 :: thesis: { S where S is Subset of K : ( S is simplex-like & v in S ) } is finite
A6: { S where S is Subset of K : ( S is simplex-like & v in S ) } c= the topology of K

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { S where S is Subset of K : ( S is simplex-like & v in S ) } or x in the topology of K )
assume x in { S where S is Subset of K : ( S is simplex-like & v in S ) } ; :: thesis: x in the topology of K
then ex S being Subset of K st
( x = S & S is simplex-like & v in S ) ;
hence x in the topology of K ; :: thesis: verum

end;

the topology of K is finite by A5, Lm6;
hence { S where S is Subset of K : ( S is simplex-like & v in S ) } is finite by A6; :: thesis: verum

end;

thus K is finite-membered :: according to MATROID0:def 7 :: thesis: ex b₁ being set st
for b₂ being Element of bool the carrier of K holds
( not b₂ is simplex-like or card b₂ <= b₁ )

proof

let x be set ; :: according to FINSET_1:def 6,MATROID0:def 6 :: thesis: ( not x in the_family_of K or x is finite )
assume A7: x in the_family_of K ; :: thesis: x is finite
then reconsider X = x as Subset of K ;
X is simplex-like by A7;
then X c= V by Lm4;
hence x is finite ; :: thesis: verum

end;

take card V ; :: thesis: for b₁ being Element of bool the carrier of K holds
( not b₁ is simplex-like or card b₁ <= card V )
let A be finite Subset of K; :: thesis: ( not A is simplex-like or card A <= card V )
assume A is open ; :: thesis: card A <= card V
hence card A <= card V by Lm4, NAT_1:43; :: thesis: verum