:: deftheorem defines are_Disomorphic GLIB_015:def 12 :
for S1, S2 being Graph-membered set holds
( S1,S2 are_Disomorphic iff ex f being one-to-one Function st
( dom f = S1 & rng f = S2 & ( for G being _Graph st G in S1 holds
f . G is b₄ -Disomorphic _Graph ) ) );