theorem :: GLIB_015:46

for G1, G2 being _Graph
for x, y being object holds
( x .--> G1,y .--> G2 are_Disomorphic iff G2 is G1 -Disomorphic )