let x be set ; :: thesis: {{},{x}} is SimpleGraph
set H = {{},{x}};
A1: {{},{x}} is 1 -at_most_dimensional

proof

let a be set ; :: according to SCMYCIEL:def 4 :: thesis: ( a in {{},{x}} implies card a c= 1 + 1 )
assume A2: a in {{},{x}} ; :: thesis: card a c= 1 + 1

per cases ( a = {} or a = {x} ) by A2, TARSKI:def 2;

suppose a = {} ; :: thesis: card a c= 1 + 1

hence card a c= 1 + 1 ; :: thesis: verum

end;

suppose a = {x} ; :: thesis: card a c= 1 + 1

then A3: card a = 1 by CARD_1:30;
Segm 1 c= Segm (1 + 1) by NAT_1:39;
hence card a c= 1 + 1 by A3; :: thesis: verum

end;

end;

end;

{{},{x}} is subset-closed

proof

let X, Y be set ; :: according to CLASSES1:def 1 :: thesis: ( not X in {{},{x}} or not Y c= X or Y in {{},{x}} )
assume that
A4: X in {{},{x}} and
A5: Y c= X ; :: thesis: Y in {{},{x}}

per cases ( X = {} or X = {x} ) by A4, TARSKI:def 2;

suppose X = {} ; :: thesis: Y in {{},{x}}

then Y = {} by A5;
hence Y in {{},{x}} by TARSKI:def 2; :: thesis: verum

end;

suppose A6: X = {x} ; :: thesis: Y in {{},{x}}

per cases ( Y = {} or Y = {x} ) by A6, A5, ZFMISC_1:33;

suppose Y = {} ; :: thesis: Y in {{},{x}}

hence Y in {{},{x}} by TARSKI:def 2; :: thesis: verum

end;

suppose Y = {x} ; :: thesis: Y in {{},{x}}

hence Y in {{},{x}} by TARSKI:def 2; :: thesis: verum

end;

end;

end;

end;

end;

hence {{},{x}} is SimpleGraph by A1; :: thesis: verum