:: deftheorem defines isomorphism GLIB_011:def 5 :
for G1, G2 being _Graph
for f being PVertexMapping of G1,G2 holds
( f is isomorphism iff ( f is total & f is one-to-one & f is onto & ( for v, w being Vertex of G1 holds card (G1 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)})) ) ) );