set PP = subdivision (P,KX);
assume subdivision (P,KX) is with_non-empty_element ; :: thesis: contradiction
then the topology of (subdivision (P,KX)) is with_non-empty_element ;
then consider x being non empty set such that
A1: x in the topology of (subdivision (P,KX)) ;
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 ;
then consider y being object such that
A3: y in S /\ (dom P) ;
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 ;
hence contradiction by PENCIL_1:def 4; :: thesis: verum