consider x being set such that
A1: x in the topology of KD by XBOOLE_0:def 1;
reconsider E = {} as Subset of KD by XBOOLE_1:2;
( E in the topology of KD & card E c= card (i + 1) ) by PRE_TOPC:def 5;
then E in the_subsets_with_limited_card ((i + 1), the topology of KD) by Def2;
hence not Skeleton_of (KD,i) is void ; :: thesis: verum