theorem :: GLIB_015:34

for G1, G2 being _Graph holds
( {G1},{G2} are_Disomorphic iff G2 is G1 -Disomorphic )