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