theorem lemoe4: :: REALALG3:37

for F being ordered Field
for E being FieldExtension of F
for P being Ordering of F holds
( P extends_to E iff QS (E,P) is prepositive_cone )