theorem fi2: :: REALALG2:51

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