theorem lemoe3: :: REALALG3:35

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