let X be set ; :: thesis: ex G being SimpleGraph st
( G is edgeless & Vertices G = X )
set G = {{}} \/ (singletons X);
A1: {{}} \/ (singletons X) is subset-closed

proof

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

per cases ( x in {{}} or x in singletons X ) by A2, XBOOLE_0:def 3;

suppose x in {{}} ; :: thesis: y in {{}} \/ (singletons X)

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: verum

end;

suppose x in singletons X ; :: thesis: y in {{}} \/ (singletons X)

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 ( y = {} or y = {v} ) by A3, A4, A6, ZFMISC_1:33;

suppose y = {} ; :: thesis: y in {{}} \/ (singletons X)

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

end;

suppose y = {v} ; :: thesis: y in {{}} \/ (singletons X)

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

end;

end;

end;

end;

end;

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

proof

let x be set ; :: according to SCMYCIEL:def 4 :: thesis: ( x in {{}} \/ (singletons X) implies card x c= 1 + 1 )
assume A8: x in {{}} \/ (singletons X) ; :: thesis: card x c= 1 + 1

per cases ( x in {{}} or x in singletons X ) by A8, XBOOLE_0:def 3;

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

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

end;

suppose x in singletons X ; :: thesis: card x c= 1 + 1

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: verum

end;

end;

end;

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

now :: thesis: not Edges G <> {}

assume Edges G <> {} ; :: thesis: contradiction
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 ( e in {{}} or e in singletons X ) by A13, XBOOLE_0:def 3;

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

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

end;

suppose e in singletons X ; :: thesis: contradiction

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: verum

end;

end;

end;

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

proof

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

proof

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

per cases ( y in {{}} or y in singletons X ) by A19, XBOOLE_0:def 3;

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

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

end;

suppose y in singletons X ; :: thesis: x in X

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: verum

end;

end;

end;

thus X c= Vertices G :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Vertices G )
assume x in X ; :: thesis: x in Vertices G
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: verum

end;

end;