for R, S being Relation
for F being Function st F is_isomorphism_of R,S holds
for a, b being object st [a,b] in R & a <> b holds
( [(F . a),(F . b)] in S & F . a <> F . b )