:: deftheorem defines are_isomorphic GLIB_015:def 15 :
for F1, F2 being Graph-yielding Function holds
( F1,F2 are_isomorphic iff ex p being one-to-one Function st
( dom p = dom F1 & rng p = dom F2 & ( for x being object st x in dom F1 holds
ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -isomorphic ) ) ) );