theorem Th1: :: PCOMPS_2:1

for R being Relation
for A being set st R well_orders A holds
( R |_2 A well_orders A & A = field (R |_2 A) )