theorem Th23: :: WELLORD1:23

for R being Relation holds R |_2 (field R) = R