let X be set ; :: thesis: for KX being SimplicialComplexStr of X
for i being dim-like number 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: for i being dim-like number st KX is subset-closed & Skeleton_of (KX,i) is empty-membered & not KX is empty-membered holds
i = - 1
let i be dim-like number ; :: 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 KX is with_non-empty_element ; :: thesis: i = - 1
then the topology of KX is with_non-empty_element ;
then consider x being non empty set such that
A3: x in the topology of KX ;
consider y being object such that
A4: y in x by XBOOLE_0:def 1;
assume i <> - 1 ; :: thesis: contradiction
then ( {} c= card (Segm (i + 1)) & not Segm (i + 1) is empty ) ;
then {} in card (Segm (i + 1)) by CARD_1:3;
then 1 c= card (Segm (i + 1)) by CARD_2:68;
then A5: card {y} c= card (Segm (i + 1)) by CARD_1:30;
{y} c= x by A4, ZFMISC_1:31;
then {y} in the topology of KX by A1, A3;
then {y} in the_subsets_with_limited_card ((Segm (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;
hence contradiction by A6; :: thesis: verum