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

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

assume A1: G2 .allSG() c= G1 .allSG() ; :: thesis: G2 is Subgraph of G1
G2 | _GraphSelectors in G2 .allSG() by Th3;
then A2: G2 | _GraphSelectors is Subgraph of G1 by A1, Th1;
G2 == G2 | _GraphSelectors by GLIB_000:128;
hence G2 is Subgraph of G1 by A2, GLIB_000:92; :: thesis: verum

end;

assume A3: G2 is Subgraph of G1 ; :: thesis: G2 .allSG() c= G1 .allSG()

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

let x be object ; :: thesis: ( x in G2 .allSG() implies x in G1 .allSG() )
assume A4: x in G2 .allSG() ; :: thesis: x in G1 .allSG()
then reconsider H = x as _Graph ;
H is Subgraph of G2 by A4, Th1;
then H is Subgraph of G1 by A3, GLIB_000:43;
hence x in G1 .allSG() by A4, Th1; :: thesis: verum

end;

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