let S be Subset-Family of K; :: thesis: ( S is simplex-like implies S is finite )
assume S is simplex-like ; :: thesis: S is finite
then A1: S c= the topology of K by Th14;
Vertices K = union the topology of K by Lm5;
then A2: the topology of K c= bool (Vertices K) by ZFMISC_1:82;
Vertices K is finite by Def5;
hence S is finite by A1, A2; :: thesis: verum