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