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

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