theorem :: REALALG2:32

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