set PP = subdivision (P,KX);
assume not subdivision (P,KX) is empty-membered ; :: thesis: contradiction
then not the topology of (subdivision (P,KX)) is empty-membered by Def7;
then consider x being non empty set such that
A1: x in the topology of (subdivision (P,KX)) by SETFAM_1:def 10;
reconsider A = x as Simplex of (subdivision (P,KX)) by A1, PRE_TOPC:def 2;
consider S being c=-linear finite simplex-like Subset-Family of KX such that
A2: A = P .: S by Def20;
A = P .: (S /\ (dom P)) by A2, RELAT_1:112;
then not S /\ (dom P) is empty by RELAT_1:116;
then consider y being set such that
A3: y in S /\ (dom P) by XBOOLE_0:def 1;
A4: y in S by A3, XBOOLE_0:def 4;
reconsider y = y as Subset of KX by A3;
y is simplex-like by A4, TOPS_2:def 1;
then y in the topology of KX by PRE_TOPC:def 2;
hence contradiction by PENCIL_1:def 4; :: thesis: verum