let G1, G2 be non-multi _Graph; :: thesis: ( G2 is G1 -isomorphic iff ex f being PVertexMapping of G1,G2 st f is isomorphism )

hereby :: thesis: ( ex f being PVertexMapping of G1,G2 st f is isomorphism implies G2 is G1 -isomorphic )

assume G2 is G1 -isomorphic ; :: thesis: ex f being PVertexMapping of G1,G2 st f is isomorphism
then consider F being PGraphMapping of G1,G2 such that
A1: F is isomorphism by GLIB_010:def 23;
consider f being PVertexMapping of G1,G2 such that
A2: ( F _V = f & f is isomorphism ) by A1, Th25;
take f = f; :: thesis: f is isomorphism
thus f is isomorphism by A2; :: thesis: verum

end;

given f being PVertexMapping of G1,G2 such that A3: f is isomorphism ; :: thesis: G2 is G1 -isomorphic
PVM2PGM f is isomorphism by A3, Th47;
hence G2 is G1 -isomorphic by GLIB_010:def 23; :: thesis: verum