let K be SimplicialComplexStr; :: thesis: ( K is finite-vertices implies the topology of K is finite )
Vertices K = union the topology of K by Lm5;
then A1: the topology of K c= bool (Vertices K) by ZFMISC_1:82;
assume K is finite-vertices ; :: thesis: the topology of K is finite
then Vertices K is finite ;
hence the topology of K is finite by A1; :: thesis: verum