theorem lemoe2: :: REALALG3:36

for F being ordered Field
for E being FieldExtension of F
for P being Ordering of F holds
( QS (E,P) is prepositive_cone iff not - (1. E) in QS (E,P) )