:: deftheorem defines are_isomorphic WELLORD1:def 8 :
for R, S being Relation holds
( R,S are_isomorphic iff ex F being Function st F is_isomorphism_of R,S );