let G1, G2 be _Graph; :: thesis: ( G1 == G2 iff G1 .allSpanningSG() = G2 .allSpanningSG() )

hereby :: thesis: ( G1 .allSpanningSG() = G2 .allSpanningSG() implies G1 == G2 )

assume A1: G1 == G2 ; :: thesis: G1 .allSpanningSG() = G2 .allSpanningSG()
then the_Vertices_of G1 = the_Vertices_of G2 by GLIB_000:def 34;
then ( G1 is spanning Subgraph of G2 & G2 is spanning Subgraph of G1 ) by A1, GLIB_000:87, GLIB_000:def 33;
then ( G1 .allSpanningSG() c= G2 .allSpanningSG() & G2 .allSpanningSG() c= G1 .allSpanningSG() ) by Th65;
hence G1 .allSpanningSG() = G2 .allSpanningSG() by XBOOLE_0:def 10; :: thesis: verum

end;

assume G1 .allSpanningSG() = G2 .allSpanningSG() ; :: thesis: G1 == G2
then ( G1 is spanning Subgraph of G2 & G2 is spanning Subgraph of G1 ) by Th65;
hence G1 == G2 by GLIB_000:87; :: thesis: verum