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 11;
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