let K be SimplicialComplexStr; :: thesis: ( K is empty-membered implies ( K is subset-closed & K is finite-vertices ) )
assume A1: K is empty-membered ; :: thesis: ( K is subset-closed & K is finite-vertices )
then A2: the topology of K is empty-membered ;
thus K is subset-closed :: thesis: K is finite-vertices

proof

let x be set ; :: according to CLASSES1:def 1,MATROID0:def 3 :: thesis: for b₁ being set holds
( not x in the_family_of K or not b₁ c= x or b₁ in the_family_of K )
let y be set ; :: thesis: ( not x in the_family_of K or not y c= x or y in the_family_of K )
assume that
A3: x in the_family_of K and
A4: y c= x ; :: thesis: y in the_family_of K
x is empty by A2, A3;
hence y in the_family_of K by A3, A4; :: thesis: verum

end;

Vertices K is empty by A1, Lm2;
hence K is finite-vertices ; :: thesis: verum