theorem Th20: :: SIMPLEX0:20

for K being SimplicialComplexStr st K is subset-closed & the topology of K is finite holds
K is finite-vertices