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

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

assume G1 == G2 ; :: thesis: G1 .allConnectedSG() = G2 .allConnectedSG()
then ( G1 is Subgraph of G2 & G2 is Subgraph of G1 ) by GLIB_000:87;
then ( G2 .allConnectedSG() c= G1 .allConnectedSG() & G1 .allConnectedSG() c= G2 .allConnectedSG() ) by Th129;
hence G1 .allConnectedSG() = G2 .allConnectedSG() by XBOOLE_0:def 10; :: thesis: verum

end;

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