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

hereby :: thesis: ( G2 is G1 -isomorphic implies {G1},{G2} are_isomorphic )

assume {G1},{G2} are_isomorphic ; :: thesis: G2 is G1 -isomorphic
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₁ -isomorphic _Graph ;
A3: f = {G1} --> G2 by A1, FUNCOP_1:9;
G1 in {G1} by TARSKI:def 1;
then ( f . G1 is G1 -isomorphic _Graph & f . G1 = G2 ) by A2, A3, FUNCOP_1:7;
hence G2 is G1 -isomorphic ; :: thesis: verum

end;

assume A4: G2 is G1 -isomorphic ; :: thesis: {G1},{G2} are_isomorphic
reconsider f = G1 .--> G2 as one-to-one Function ;
take f ; :: according to GLIB_015:def 13 :: thesis: ( dom f = {G1} & rng f = {G2} & ( for G being _Graph st G in {G1} holds
f . G is b₁ -isomorphic _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₁ -isomorphic _Graph
let G be _Graph; :: thesis: ( G in {G1} implies f . G is G -isomorphic _Graph )
assume G in {G1} ; :: thesis: f . G is G -isomorphic _Graph
then G = G1 by TARSKI:def 1;
hence f . G is G -isomorphic _Graph by A4, FUNCOP_1:72; :: thesis: verum