:: deftheorem defines is_isomorphism_of WELLORD1:def 7 :
for R, S being Relation
for F being Function holds
( F is_isomorphism_of R,S iff ( dom F = field R & rng F = field S & F is one-to-one & ( for a, b being object holds
( [a,b] in R iff ( a in field R & b in field R & [(F . a),(F . b)] in S ) ) ) ) );