assume Skeleton_of (KX,(- 1)) is with_non-empty_element ; :: thesis: contradiction
then the topology of (Skeleton_of (KX,(- 1))) is with_non-empty_element ;
then consider x being non empty set such that
A1: x in the topology of (Skeleton_of (KX,(- 1))) ;
consider b being set such that
A2: x c= b and
A3: b in the_subsets_with_limited_card ((Segm ((- 1) + 1)), the topology of KX) by A1, Th2;
card b c= card (Segm ((- 1) + 1)) by A3, Def2;
then card b c= {} ;
then b is empty ;
hence contradiction by A2; :: thesis: verum