let K be SimplicialComplexStr; :: thesis: ( K is subset-closed & the topology of K is finite implies K is finite-vertices )
assume that
A1: K is subset-closed and
A2: the topology of K is finite ; :: thesis: K is finite-vertices
assume not K is finite-vertices ; :: thesis: contradiction
then not K is finite-membered by A2, Th19;
then not the_family_of K is finite-membered ;
then consider x being set such that
A3: x in the_family_of K and
A4: not x is finite ;
{x} c= the_family_of K by A3, ZFMISC_1:31;
then subset-closed_closure_of {x} c= the_family_of K by A1, Th3;
then bool x c= the_family_of K by Th4;
hence contradiction by A2, A4; :: thesis: verum