theorem fi1: :: REALALG2:50

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 " )