:: deftheorem Def9 defines canonical_isomorphism_of WELLORD1:def 9 :
for R, S being Relation st R is well-ordering & R,S are_isomorphic holds
for b₃ being Function holds
( b₃ = canonical_isomorphism_of (R,S) iff b₃ is_isomorphism_of R,S );