theorem T3: :: REALALG2:29

for F being preordered Field
for P being Preordering of F ex Q being Preordering of F st
( P c= Q & Q is maximal )