let R be Relation; :: thesis: R,R are_isomorphic
take id (field R) ; :: according to WELLORD1:def 8 :: thesis: id (field R) is_isomorphism_of R,R
thus id (field R) is_isomorphism_of R,R by Th37; :: thesis: verum