for G1, G2 being non-Dmulti _Graph holds
( G2 is G1 -Disomorphic iff ex f being directed PVertexMapping of G1,G2 st f is Disomorphism )