theorem lemoe1: :: REALALG3:34

for F being ordered Field
for E being FieldExtension of F
for P being Ordering of F holds P c= QS (E,P)