theorem main: :: REALALG3:50

for F being ordered Field
for P being Ordering of F
for E being FieldExtension of F st deg (E,F) is odd Nat holds
P extends_to E