theorem T1a: :: REALALG2:31

for F being preordered Field
for P being Preordering of F ex O being Ordering of F st P c= O