let G1 be _Graph; :: thesis: for G2 being G1 -isomorphic _Graph holds G1 is G2 -isomorphic

let G2 be G1 -isomorphic _Graph; :: thesis: G1 is G2 -isomorphic

consider F being PGraphMapping of G1,G2 such that

A1: F is isomorphism by Def23;

reconsider F = F as one-to-one PGraphMapping of G1,G2 by A1;

take F " ; :: according to GLIB_010:def 23 :: thesis: F " is isomorphism

thus F " is isomorphism by A1, Th75; :: thesis: verum

let G2 be G1 -isomorphic _Graph; :: thesis: G1 is G2 -isomorphic

consider F being PGraphMapping of G1,G2 such that

A1: F is isomorphism by Def23;

reconsider F = F as one-to-one PGraphMapping of G1,G2 by A1;

take F " ; :: according to GLIB_010:def 23 :: thesis: F " is isomorphism

thus F " is isomorphism by A1, Th75; :: thesis: verum