let G be _Graph; :: thesis: the_Edges_of (G .allSG()) = bool (the_Edges_of G)

now :: thesis: for x being object holds
( ( x in the_Edges_of (G .allSG()) implies x in bool (the_Edges_of G) ) & ( x in bool (the_Edges_of G) implies x in the_Edges_of (G .allSG()) ) )

let x be object ; :: thesis: ( ( x in the_Edges_of (G .allSG()) implies x in bool (the_Edges_of G) ) & ( x in bool (the_Edges_of G) implies x in the_Edges_of (G .allSG()) ) )

hereby :: thesis: ( x in bool (the_Edges_of G) implies x in the_Edges_of (G .allSG()) )

assume x in the_Edges_of (G .allSG()) ; :: thesis: x in bool (the_Edges_of G)
then consider H being _Graph such that
A1: ( H in G .allSG() & x = the_Edges_of H ) by GLIB_014:def 15;
H is Subgraph of G by A1, Th1;
then the_Edges_of H c= the_Edges_of G by GLIB_000:def 32;
hence x in bool (the_Edges_of G) by A1; :: thesis: verum

end;

reconsider X = x as set by TARSKI:1;
set H = the plain inducedSubgraph of G, the_Vertices_of G,X;
assume x in bool (the_Edges_of G) ; :: thesis: x in the_Edges_of (G .allSG())
then X c= the_Edges_of G ;
then A2: X c= G .edgesBetween (the_Vertices_of G) by GLIB_000:34;
the_Vertices_of G c= the_Vertices_of G ;
then A3: the_Edges_of the plain inducedSubgraph of G, the_Vertices_of G,X = X by A2, GLIB_000:def 37;
the plain inducedSubgraph of G, the_Vertices_of G,X in G .allSG() by Th1;
hence x in the_Edges_of (G .allSG()) by A3, GLIB_014:def 15; :: thesis: verum

end;

hence the_Edges_of (G .allSG()) = bool (the_Edges_of G) by TARSKI:2; :: thesis: verum