theorem :: REALALG2:32
for F being ordered Field
for P being Preordering of F holds /\ (P,F) is Preordering of F ;