theorem T2: :: REALALG2:27

for F being preordered Field
for P being Preordering of F
for a being Element of F st not - a in P holds
P + (a * P) is Preordering of F