let G1, G2 be _Graph; :: thesis: ( G2 .allSpanningSG() c= G1 .allSpanningSG() iff G2 is spanning Subgraph of G1 )

hereby :: thesis: ( G2 is spanning Subgraph of G1 implies G2 .allSpanningSG() c= G1 .allSpanningSG() )

assume A1: G2 .allSpanningSG() c= G1 .allSpanningSG() ; :: thesis: G2 is spanning Subgraph of G1
G2 | _GraphSelectors in G2 .allSpanningSG() by Th62;
then G2 | _GraphSelectors is spanning Subgraph of G1 by A1, Th60;
hence G2 is spanning Subgraph of G1 by GLIB_000:171, GLIB_000:128; :: thesis: verum

end;

assume A2: G2 is spanning Subgraph of G1 ; :: thesis: G2 .allSpanningSG() c= G1 .allSpanningSG()

now :: thesis: for x being object st x in G2 .allSpanningSG() holds
x in G1 .allSpanningSG()

let x be object ; :: thesis: ( x in G2 .allSpanningSG() implies x in G1 .allSpanningSG() )
assume x in G2 .allSpanningSG() ; :: thesis: x in G1 .allSpanningSG()
then reconsider H = x as spanning plain Subgraph of G2 by Th60;
the_Vertices_of H = the_Vertices_of G2 by GLIB_000:def 33
.= the_Vertices_of G1 by A2, GLIB_000:def 33 ;
then H is spanning plain Subgraph of G1 by A2, GLIB_000:43, GLIB_000:def 33;
hence x in G1 .allSpanningSG() by Th60; :: thesis: verum

end;

hence G2 .allSpanningSG() c= G1 .allSpanningSG() by TARSKI:def 3; :: thesis: verum