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 11;
reconsider A = x as Simplex of (subdivision P,KX) by A1, PRE_TOPC:def 5;
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:145;
then not S /\ (dom P) is empty by RELAT_1:149;
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 5;
hence contradiction by PENCIL_1:def 4; :: thesis: verum