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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in G or x in ({{}} \/ (singletons (Vertices G))) \/ (Edges G) )
assume A1: x in G ; :: thesis: x in ({{}} \/ (singletons (Vertices G))) \/ (Edges G)
reconsider v = x as finite set by A1;
card v <= 1 + 1 by A1, Th21;
then not not card v = 0 & ... & not card v = 2 ;

per cases then ( card v = 0 or card v = 1 or card v = 2 ) ;

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 object such that
A2: v = {a} by CARD_2:42;
A3: a in v by A2, TARSKI:def 1;
A4: a in union G by A3, A1, TARSKI:def 4;
reconsider v = v as Subset of (Vertices G) by A4, A2, ZFMISC_1:31;
v in singletons (Vertices G) by A2;
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 A1, Def1;
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 object ; :: 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 A5: ( 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 A5, XBOOLE_0:def 3;

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

consider z being object such that
A7: z in G by XBOOLE_0:def 1;
reconsider z = z as set by TARSKI:1;
A8: {} c= z ;
x = {} by A6, TARSKI:def 1;
hence x in G by A8, A7, 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
A9: x = f and
A10: f is 1 -element ;
consider v being set such that
A11: v in Vertices G and
A12: f = {v} by A10, Th9;
thus x in G by A9, A11, A12, Th24; :: thesis: verum

end;

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

hence x in G ; :: thesis: verum

end;

end;

end;