reconsider V = Vertices KX as finite Subset of KX by Def5;
set PP = subdivision P,KX;
set TOP = the topology of (subdivision P,KX);
defpred S₁[ set , set ] means P .: KX = X;
bool V = bool (union the topology of KX) by Lm5;
then A1: the topology of KX c= bool V by ZFMISC_1:100;
A2: for x being set st x in the topology of (subdivision P,KX) holds
ex y being set st
( y in bool (bool V) & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in the topology of (subdivision P,KX) implies ex y being set st
( y in bool (bool V) & S₁[x,y] ) )
assume A3: x in the topology of (subdivision P,KX) ; :: thesis: ex y being set st
( y in bool (bool V) & S₁[x,y] )
reconsider X = x as Subset of (subdivision P,KX) by A3;
X is simplex-like by A3, PRE_TOPC:def 5;
then consider S being c=-linear finite simplex-like Subset-Family of KX such that
A4: X = P .: S by Def20;
take S ; :: thesis: ( S in bool (bool V) & S₁[x,S] )
S c= the topology of KX

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in S or y in the topology of KX )
assume A5: y in S ; :: thesis: y in the topology of KX
reconsider Y = y as Subset of KX by A5;
Y is simplex-like by A5, TOPS_2:def 1;
hence y in the topology of KX by PRE_TOPC:def 5; :: thesis: verum

end;

then S c= bool V by A1, XBOOLE_1:1;
hence ( S in bool (bool V) & S₁[x,S] ) by A4; :: thesis: verum

end;

consider f being Function of the topology of (subdivision P,KX),(bool (bool V)) such that
A6: for x being set st x in the topology of (subdivision P,KX) holds
S₁[x,f . x] from FUNCT_2:sch 1(A2);

now

let x1, x2 be set ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A7: x1 in dom f and
A8: ( x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
thus x1 = P .: (f . x1) by A6, A7
.= x2 by A6, A8 ; :: thesis: verum

end;

then A9: f is one-to-one by FUNCT_1:def 8;
( dom f = the topology of (subdivision P,KX) & rng f c= bool (bool V) ) by FUNCT_2:def 1;
then card the topology of (subdivision P,KX) c= card (bool (bool V)) by A9, CARD_1:26;
then the topology of (subdivision P,KX) is finite ;
hence subdivision P,KX is finite-vertices by Th20; :: thesis: verum