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 ) ;
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;
end;
end;