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