let G be SimpleGraph; :: thesis: G = ({{}} \/ (singletons (Vertices G))) \/ (Edges G)
thus G c= ({{}} \/ (singletons (Vertices G))) \/ (Edges G) :: according to XBOOLE_0:def 10 :: thesis: ({{}} \/ (singletons (Vertices G))) \/ (Edges G) c= G

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in G or x in ({{}} \/ (singletons (Vertices G))) \/ (Edges G) )
assume A: x in G ; :: thesis: x in ({{}} \/ (singletons (Vertices G))) \/ (Edges G)
reconsider v = x as finite set by A;
B: card v <= 1 + 1 by A, Lnatmost1;

per cases ( card v = 0 or card v = 1 or card v = 2 ) by B, NAT_1:26;

suppose card v = 0 ; :: thesis: x in ({{}} \/ (singletons (Vertices G))) \/ (Edges G)

then v = {} ;
then v in {{}} by TARSKI:def 1;
then v in {{}} \/ (singletons (Vertices G)) by XBOOLE_0:def 3;
hence x in ({{}} \/ (singletons (Vertices G))) \/ (Edges G) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose card v = 1 ; :: thesis: x in ({{}} \/ (singletons (Vertices G))) \/ (Edges G)

then consider a being set such that
A1: v = {a} by CARD_2:42;
B1: a in v by A1, TARSKI:def 1;
C1: a in union G by B1, A, TARSKI:def 4;
reconsider v = v as Subset of (Vertices G) by C1, A1, ZFMISC_1:31;
v in singletons (Vertices G) by A1;
then v in {{}} \/ (singletons (Vertices G)) by XBOOLE_0:def 3;
hence x in ({{}} \/ (singletons (Vertices G))) \/ (Edges G) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose card v = 2 ; :: thesis: x in ({{}} \/ (singletons (Vertices G))) \/ (Edges G)

then v in Edges G by A, LEdges;
hence x in ({{}} \/ (singletons (Vertices G))) \/ (Edges G) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

thus ({{}} \/ (singletons (Vertices G))) \/ (Edges G) c= G :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ({{}} \/ (singletons (Vertices G))) \/ (Edges G) or x in G )
assume x in ({{}} \/ (singletons (Vertices G))) \/ (Edges G) ; :: thesis: x in G
then A1: ( x in {{}} \/ (singletons (Vertices G)) or x in Edges G ) by XBOOLE_0:def 3;

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

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

consider z being set such that
A2: z in G by XBOOLE_0:def 1;
B2: {} c= z by XBOOLE_1:2;
x = {} by S1, TARSKI:def 1;
hence x in G by B2, A2, CLASSES1:def 1; :: thesis: verum

end;

suppose x in singletons (Vertices G) ; :: thesis: x in G

then consider f being Subset of (Vertices G) such that
A2: x = f and
B2: f is 1 -element ;
consider v being set such that
C2: v in Vertices G and
D2: f = {v} by B2, BSPACEdef9;
thus x in G by A2, C2, D2, Vertices0; :: thesis: verum

end;

suppose x in Edges G ; :: thesis: x in G

hence x in G ; :: thesis: verum

end;

end;

end;