let x be set ; :: thesis: {{},{x}} is SimpleGraph
set H = {{},{x}};
B: {{},{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 A1: a in {{},{x}} ; :: thesis: card a c= 1 + 1

per cases ( a = {} or a = {x} ) by A1, 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 card a = 1 by CARD_1:30;
hence card a c= 1 + 1 by NAT_1:39; :: 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
A1: X in {{},{x}} and
B1: Y c= X ; :: thesis: Y in {{},{x}}

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

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

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

end;

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

per cases ( Y = {} or Y = {x} ) by S1, B1, 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 B; :: thesis: verum