theorem Th37: :: WELLORD1:37

for R being Relation holds id (field R) is_isomorphism_of R,R