:: deftheorem Def24 defines -Disomorphic GLIB_010:def 24 :
for G1, G2 being _Graph holds
( G2 is G1 -Disomorphic iff ex F being PGraphMapping of G1,G2 st F is Disomorphism );