theorem :: REALALG2:33

for F being ordered Field
for P being Preordering of F holds /\ (P,F) = P by s1;