let X be set ; :: thesis: for i being Integer
for KX being SimplicialComplexStr of X st KX is subset-closed & Skeleton_of (KX,i) is empty-membered & not KX is empty-membered holds
i = - 1
let i be Integer; :: thesis: for KX being SimplicialComplexStr of X st KX is subset-closed & Skeleton_of (KX,i) is empty-membered & not KX is empty-membered holds
i = - 1
let KX be SimplicialComplexStr of X; :: thesis: ( KX is subset-closed & Skeleton_of (KX,i) is empty-membered & not KX is empty-membered implies i = - 1 )
assume KX is subset-closed ; :: thesis: ( not Skeleton_of (KX,i) is empty-membered or KX is empty-membered or i = - 1 )
then A1: the_family_of KX is subset-closed ;
assume A2: Skeleton_of (KX,i) is empty-membered ; :: thesis: ( KX is empty-membered or i = - 1 )
assume not KX is empty-membered ; :: thesis: i = - 1
then not the topology of KX is empty-membered by Def7;
then consider x being non empty set such that
A3: x in the topology of KX by SETFAM_1:def 10;
consider y being set such that
A4: y in x by XBOOLE_0:def 1;
assume i <> - 1 ; :: thesis: contradiction
then ( {} c= card (i + 1) & not i + 1 is empty ) ;
then {} in card (i + 1) by CARD_1:3;
then 1 c= card (i + 1) by CARD_2:68;
then A5: card {y} c= card (i + 1) by CARD_1:30;
{y} c= x by A4, ZFMISC_1:31;
then {y} in the topology of KX by A1, A3, CLASSES1:def 1;
then {y} in the_subsets_with_limited_card ((i + 1), the topology of KX) by A5, Def2;
then A6: {y} in the topology of (Skeleton_of (KX,i)) by Th2;
the topology of (Skeleton_of (KX,i)) is empty-membered by A2, Def7;
hence contradiction by A6, SETFAM_1:def 10; :: thesis: verum