theorem ord5: :: REALALG1:27

for F being preordered Field
for P being Preordering of F
for a being non zero Element of F st a in P holds
a " in P