:: deftheorem defines are_isomorphic GLIB_015:def 13 :
for S1, S2 being Graph-membered set holds
( S1,S2 are_isomorphic 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₄ -isomorphic _Graph ) ) );