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