let SX be SubSimplicialComplex of KX; :: thesis: SX is finite-vertices
A1: Vertices KX is finite by Def5;
the topology of SX c= the topology of KX by Def13;
then A2: union the topology of SX c= union the topology of KX by ZFMISC_1:77;
( union the topology of SX = Vertices SX & union the topology of KX = Vertices KX ) by Lm5;
hence SX is finite-vertices by A2, A1; :: thesis: verum