for G1, G2 being non-multi _Graph holds
( G2 is G1 -isomorphic iff ex f being PVertexMapping of G1,G2 st f is isomorphism )