let K be SimplicialComplexStr; :: thesis: ( K is empty-membered implies ( K is subset-closed & K is finite-vertices ) )
assume A2: K is empty-membered ; :: thesis: ( K is subset-closed & K is finite-vertices )
then A3: the topology of K is empty-membered by Def7;
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
A4: x in the_family_of K and
A5: y c= x ; :: thesis: y in the_family_of K
x is empty by A3, A4, SETFAM_1:def 11;
hence y in the_family_of K by A4, A5; :: thesis: verum

end;

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