let G1, G2 be _Graph; :: thesis: ( G1 == G2 iff G1 .allInducedSG() = G2 .allInducedSG() )
set V1 = the_Vertices_of G1;
set V2 = the_Vertices_of G2;

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

assume A1: G1 == G2 ; :: thesis: G1 .allInducedSG() = G2 .allInducedSG()
( G1 is inducedSubgraph of G1,(the_Vertices_of G1) & G2 is inducedSubgraph of G2,(the_Vertices_of G2) ) by GLIB_000:100;
then A2: ( G1 is inducedSubgraph of G2,(the_Vertices_of G2) & G2 is inducedSubgraph of G1,(the_Vertices_of G1) ) by A1, GLIB_000:101;
( the_Vertices_of G1 c= the_Vertices_of G1 & the_Vertices_of G2 c= the_Vertices_of G2 ) ;
then ( G1 .allInducedSG() c= G2 .allInducedSG() & G2 .allInducedSG() c= G1 .allInducedSG() ) by A2, Th48;
hence G1 .allInducedSG() = G2 .allInducedSG() by XBOOLE_0:def 10; :: thesis: verum

end;

assume A3: G1 .allInducedSG() = G2 .allInducedSG() ; :: thesis: G1 == G2
then consider V2 being non empty Subset of (the_Vertices_of G2) such that
A4: G1 is inducedSubgraph of G2,V2 by Th48;
consider V1 being non empty Subset of (the_Vertices_of G1) such that
A5: G2 is inducedSubgraph of G1,V1 by A3, Th48;
thus G1 == G2 by A4, A5, GLIB_000:87; :: thesis: verum