let G be _Graph; :: thesis: the_Edges_of (G .allSpanningSG()) = bool (the_Edges_of G)
the_Edges_of (G .allSpanningSG()) c= the_Edges_of (G .allSG()) by GLIBPRE1:115;
then A1: the_Edges_of (G .allSpanningSG()) c= bool (the_Edges_of G) by Th38;

now :: thesis: for x being object st x in bool (the_Edges_of G) holds
x in the_Edges_of (G .allSpanningSG())

let x be object ; :: thesis: ( x in bool (the_Edges_of G) implies x in the_Edges_of (G .allSpanningSG()) )
reconsider X = x as set by TARSKI:1;
assume x in bool (the_Edges_of G) ; :: thesis: x in the_Edges_of (G .allSpanningSG())
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_Vertices_of G is non empty Subset of (the_Vertices_of G) ;
set H = the plain inducedSubgraph of G, the_Vertices_of G,X;
the_Vertices_of the plain inducedSubgraph of G, the_Vertices_of G,X = the_Vertices_of G by A2, A3, GLIB_000:def 37;
then the plain inducedSubgraph of G, the_Vertices_of G,X is spanning by GLIB_000:def 33;
then A4: the plain inducedSubgraph of G, the_Vertices_of G,X in G .allSpanningSG() by Th60;
the_Edges_of the plain inducedSubgraph of G, the_Vertices_of G,X = X by A2, A3, GLIB_000:def 37;
hence x in the_Edges_of (G .allSpanningSG()) by A4, GLIB_014:def 15; :: thesis: verum

end;

then bool (the_Edges_of G) c= the_Edges_of (G .allSpanningSG()) by TARSKI:def 3;
hence the_Edges_of (G .allSpanningSG()) = bool (the_Edges_of G) by A1, XBOOLE_0:def 10; :: thesis: verum