:: deftheorem defines Disomorphism GLIB_011:def 8 :
for G1, G2 being non-Dmulti _Graph
for f being PVertexMapping of G1,G2 holds
( f is Disomorphism iff ( f is total & f is one-to-one & f is onto & f is directed & f is Dcontinuous ) );