let G1, G2 be _Graph; :: thesis: ( G2 is G1 -isomorphic implies G1 .allInducedSG() ,G2 .allInducedSG() are_isomorphic )
assume G2 is G1 -isomorphic ; :: thesis: G1 .allInducedSG() ,G2 .allInducedSG() are_isomorphic
then consider F being PGraphMapping of G1,G2 such that
A1: F is isomorphism by GLIB_010:def 23;
set f = (SG2SGFunc F) | (G1 .allInducedSG());
A2: dom ((SG2SGFunc F) | (G1 .allInducedSG())) = G1 .allInducedSG() by FUNCT_2:def 1;
A3: rng ((SG2SGFunc F) | (G1 .allInducedSG())) = G2 .allInducedSG() by A1, Th52;
SG2SGFunc F is one-to-one by A1, Th31;
then A4: (SG2SGFunc F) | (G1 .allInducedSG()) is one-to-one by FUNCT_1:52;

now :: thesis: for G being _Graph st G in G1 .allInducedSG() holds
((SG2SGFunc F) | (G1 .allInducedSG())) . G is b₁ -isomorphic _Graph

let G be _Graph; :: thesis: ( G in G1 .allInducedSG() implies ((SG2SGFunc F) | (G1 .allInducedSG())) . G is G -isomorphic _Graph )
assume A5: G in G1 .allInducedSG() ; :: thesis: ((SG2SGFunc F) | (G1 .allInducedSG())) . G is G -isomorphic _Graph
then consider V being non empty Subset of (the_Vertices_of G1) such that
A6: G is plain inducedSubgraph of G1,V by Th45;
reconsider H = G as plain inducedSubgraph of G1,V by A6;
reconsider F9 = F | H as PGraphMapping of H, rng (F | H) by GLIBPRE1:88;
A7: ((SG2SGFunc F) | (G1 .allInducedSG())) . G = (SG2SGFunc F) . G by A5, FUNCT_1:49
.= rng (F | H) by Def5 ;
F9 is isomorphism by A1, GLIBPRE1:110;
hence ((SG2SGFunc F) | (G1 .allInducedSG())) . G is G -isomorphic _Graph by A7, GLIB_010:def 23; :: thesis: verum

end;

hence G1 .allInducedSG() ,G2 .allInducedSG() are_isomorphic by A2, A3, A4, GLIB_015:def 13; :: thesis: verum