theorem :: REALALG2:60

for F being preordered Field
for P being Preordering of F
for a, b being non zero Element of F st 0. F <= P,a & 0. F <= P,b holds
( a < P,b iff b " < P,a " )