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

proof

let a be set ; :: according to SCMYCIEL:def 4 :: thesis:
assume A2: a in {{},{x}} ; :: thesis:

per cases by A2, TARSKI:def 2;

suppose a = {} ; :: thesis:

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

end;

suppose a = {x} ; :: thesis:

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:

end;

end;

end;

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

proof

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

per cases by A4, TARSKI:def 2;

suppose X = {} ; :: thesis:

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

end;

suppose A6: X = {x} ; :: thesis:

per cases by A6, A5, ZFMISC_1:33;

suppose Y = {} ; :: thesis:

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

end;

suppose Y = {x} ; :: thesis:

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

end;

end;

end;

end;

end;

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