let G1, G2 be _Graph; :: thesis: ( {G1},{G2} are_Disomorphic iff G2 is G1 -Disomorphic )

hereby :: thesis: ( G2 is G1 -Disomorphic implies {G1},{G2} are_Disomorphic )

assume {G1},{G2} are_Disomorphic ; :: thesis: G2 is G1 -Disomorphic
then consider f being one-to-one Function such that
A1: ( dom f = {G1} & rng f = {G2} ) and
A2: for G being _Graph st G in {G1} holds
f . G is b₁ -Disomorphic _Graph ;
A3: f = {G1} --> G2 by A1, FUNCOP_1:9;
G1 in {G1} by TARSKI:def 1;
then ( f . G1 is G1 -Disomorphic _Graph & f . G1 = G2 ) by A2, A3, FUNCOP_1:7;
hence G2 is G1 -Disomorphic ; :: thesis: verum

end;

assume A4: G2 is G1 -Disomorphic ; :: thesis: {G1},{G2} are_Disomorphic
reconsider f = G1 .--> G2 as one-to-one Function ;
take f ; :: according to GLIB_015:def 12 :: thesis: ( dom f = {G1} & rng f = {G2} & ( for G being _Graph st G in {G1} holds
f . G is b₁ -Disomorphic _Graph ) )
f = {G1} --> G2 by FUNCOP_1:def 9;
hence ( dom f = {G1} & rng f = {G2} ) by FUNCOP_1:8; :: thesis: for G being _Graph st G in {G1} holds
f . G is b₁ -Disomorphic _Graph
let G be _Graph; :: thesis: ( G in {G1} implies f . G is G -Disomorphic _Graph )
assume G in {G1} ; :: thesis: f . G is G -Disomorphic _Graph
then G = G1 by TARSKI:def 1;
hence f . G is G -Disomorphic _Graph by A4, FUNCOP_1:72; :: thesis: verum