:: deftheorem defines are_Disomorphic GLIB_015:def 16 :
for I being set
for F1, F2 being Graph-yielding ManySortedSet of I holds
( F1,F2 are_Disomorphic iff ex p being Permutation of I st
for x being object st x in I holds
ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -Disomorphic ) );