let X be set ; :: thesis: ex G being SimpleGraph st
( G is edgeless & Vertices G = X )
set G = {{}} \/ (singletons X);
A: {{}} \/ (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
A1: x in {{}} \/ (singletons X) and
B1: y c= x ; :: thesis: y in {{}} \/ (singletons X)

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

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

then x = {} by TARSKI:def 1;
then y = {} by B1;
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
A2: x = f and
B2: f is 1 -element ;
consider v being set such that
v in X and
D2: f = {v} by B2, BSPACEdef9;

per cases ( y = {} or y = {v} ) by B1, A2, D2, 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 A1, D2, A2; :: thesis: verum

end;

end;

end;

end;

end;

B: {{}} \/ (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 Aa: x in {{}} \/ (singletons X) ; :: thesis: card x c= 1 + 1

per cases ( x in {{}} or x in singletons X ) by Aa, 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
A2: x = f and
B2: f is 1 -element ;
consider v being set such that
v in X and
D2: f = {v} by B2, BSPACEdef9;
card x = 1 by A2, D2, CARD_1:30;
hence card x c= 1 + 1 by NAT_1:39; :: thesis: verum

end;

end;

end;

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

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

assume Edges G <> {} ; :: thesis: contradiction
then consider e being set such that
A: e in Edges G by XBOOLE_0:def 1;
B: ( e in G & card e = 2 ) by A, LEdges;

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

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

hence contradiction by B, 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
A2: e = f and
B2: f is 1 -element ;
consider v being set such that
v in X and
D2: f = {v} by B2, BSPACEdef9;
thus contradiction by B, A2, D2, CARD_1:30; :: thesis: verum

end;

end;

end;

hence G is edgeless by Ledgeless; :: 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 set ; :: 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
A1: x in y and
B1: y in G by TARSKI:def 4;

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

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

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

end;

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

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

end;

end;

end;

thus X c= Vertices G :: thesis: verum

proof

let x be set ; :: 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 Vertices0; :: thesis: verum

end;

end;