let X be set ; :: thesis:
set G = {{}} \/ (singletons X);
A1: {{}} \/ (singletons X) is subset-closed

proof

let x, y be set ; :: according to CLASSES1:def 1 :: thesis:
assume that
A2: x in {{}} \/ (singletons X) and
A3: y c= x ; :: thesis:

per cases by A2, XBOOLE_0:def 3;

suppose x in {{}} ; :: thesis:

then x = {} by TARSKI:def 1;
then y = {} by A3;
then y in {{}} by TARSKI:def 1;
hence y in {{}} \/ (singletons X) by XBOOLE_0:def 3; :: thesis:

end;

suppose x in singletons X ; :: thesis:

then consider f being Subset of X such that
A4: x = f and
A5: f is 1 -element ;
consider v being set such that
v in X and
A6: f = {v} by A5, Th9;

per cases by A3, A4, A6, ZFMISC_1:33;

suppose y = {} ; :: thesis:

then y in {{}} by TARSKI:def 1;
hence y in {{}} \/ (singletons X) by XBOOLE_0:def 3; :: thesis:

end;

suppose y = {v} ; :: thesis:

hence y in {{}} \/ (singletons X) by A2, A6, A4; :: thesis:

end;

end;

end;

end;

end;

A7: {{}} \/ (singletons X) is 1 -at_most_dimensional

proof

let x be set ; :: according to SCMYCIEL:def 4 :: thesis:
assume A8: x in {{}} \/ (singletons X) ; :: thesis:

per cases by A8, XBOOLE_0:def 3;

suppose x in {{}} ; :: thesis:

then x = {} by TARSKI:def 1;
hence card x c= 1 + 1 ; :: thesis:

end;

suppose x in singletons X ; :: thesis:

then consider f being Subset of X such that
A9: x = f and
A10: f is 1 -element ;
consider v being set such that
v in X and
A11: f = {v} by A10, Th9;
A12: card x = 1 by A9, A11, CARD_1:30;
Segm 1 c= Segm (1 + 1) by NAT_1:39;
hence card x c= 1 + 1 by A12; :: thesis:

end;

end;

end;

reconsider G = {{}} \/ (singletons X) as SimpleGraph by A1, A7;
take G ; :: thesis:

now :: thesis:

assume Edges G <> {} ; :: thesis:
then consider e being object such that
A13: e in Edges G by XBOOLE_0:def 1;
reconsider e = e as set by TARSKI:1;
A14: ( e in G & card e = 2 ) by A13, Def1;

per cases by A13, XBOOLE_0:def 3;

suppose e in {{}} ; :: thesis:

hence contradiction by A14, CARD_1:27, TARSKI:def 1; :: thesis:

end;

suppose e in singletons X ; :: thesis:

then consider f being Subset of X such that
A15: e = f and
A16: f is 1 -element ;
consider v being set such that
v in X and
A17: f = {v} by A16, Th9;
thus contradiction by A14, A15, A17, CARD_1:30; :: thesis:

end;

end;

end;

hence G is edgeless ; :: thesis:
thus Vertices G = X :: thesis:

proof

thus Vertices G c= X :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in Vertices G ; :: thesis:
then consider y being set such that
A18: x in y and
A19: y in G by TARSKI:def 4;

per cases by A19, XBOOLE_0:def 3;

suppose y in {{}} ; :: thesis:

hence x in X by A18, TARSKI:def 1; :: thesis:

end;

suppose y in singletons X ; :: thesis:

then consider f being Subset of X such that
A20: y = f and
f is 1 -element ;
thus x in X by A20, A18; :: thesis:

end;

end;

end;

thus X c= Vertices G :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in X ; :: thesis:
then reconsider f = {x} as Subset of X by ZFMISC_1:31;
f is 1 -element ;
then {x} in singletons X ;
then {x} in G by XBOOLE_0:def 3;
hence x in Vertices G by Th24; :: thesis:

end;

end;