theorem :: REALALG3:28

for F being ordered Field
for E being ordered FieldExtension of F
for P being Ordering of F
for O being Ordering of E holds
( O extends P iff for a being Element of F holds
( a in P iff a in O ) ) by XBOOLE_0:def 4, l12;