let G1, G2 be _Graph; :: thesis: ( G2 is G1 -Disomorphic implies G1 .allSG() ,G2 .allSG() are_Disomorphic )
assume G2 is G1 -Disomorphic ; :: thesis: G1 .allSG() ,G2 .allSG() are_Disomorphic
then consider F being PGraphMapping of G1,G2 such that
A1: F is Disomorphism by GLIB_010:def 24;
A2: dom (SG2SGFunc F) = G1 .allSG() by FUNCT_2:def 1;
A3: rng (SG2SGFunc F) = G2 .allSG() by A1, Th32;
A4: SG2SGFunc F is one-to-one by A1, Th31;

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

let G be _Graph; :: thesis: ( G in G1 .allSG() implies (SG2SGFunc F) . G is G -Disomorphic _Graph )
assume G in G1 .allSG() ; :: thesis: (SG2SGFunc F) . G is G -Disomorphic _Graph
then reconsider H = G as plain Subgraph of G1 by Th1;
reconsider F9 = F | H as PGraphMapping of H, rng (F | H) by GLIBPRE1:88;
A5: (SG2SGFunc F) . G = rng (F | H) by Def5;
F9 is Disomorphism by A1, GLIBPRE1:110;
hence (SG2SGFunc F) . G is G -Disomorphic _Graph by A5, GLIB_010:def 24; :: thesis: verum

end;

hence G1 .allSG() ,G2 .allSG() are_Disomorphic by A2, A3, A4, GLIB_015:def 12; :: thesis: verum