let F be ordered Field; :: thesis: for E being FieldExtension of F
for P being Ordering of F holds
( P extends_to E iff QS (E,P) is prepositive_cone )
let E be FieldExtension of F; :: thesis: for P being Ordering of F holds
( P extends_to E iff QS (E,P) is prepositive_cone )
let P be Ordering of F; :: thesis: ( P extends_to E iff QS (E,P) is prepositive_cone )

A: now :: thesis: ( P extends_to E implies QS (E,P) is prepositive_cone )

assume P extends_to E ; :: thesis: QS (E,P) is prepositive_cone
then consider O being Subset of E such that
B0: ( P c= O & O is positive_cone ) ;
reconsider E1 = E as ordered FieldExtension of F by B0, REALALG1:def 17;
reconsider O = O as Ordering of E1 by B0;
B1: QS (E,P) c= O by B0, l13, lemoe3;
not - (1. E) in O by REALALG1:26;
hence QS (E,P) is prepositive_cone by B1, lemoe2; :: thesis: verum

end;

now :: thesis: ( QS (E,P) is prepositive_cone implies P extends_to E )

assume B0: QS (E,P) is prepositive_cone ; :: thesis: P extends_to E
then reconsider E1 = E as preordered Field by REALALG1:def 16;
reconsider Pr = QS (E,P) as Preordering of E1 by B0;
consider O being Ordering of E1 such that
B1: Pr c= O by REALALG2:31;
P c= Pr by lemoe1;
then P c= O by B1;
hence P extends_to E ; :: thesis: verum

end;

hence ( P extends_to E iff QS (E,P) is prepositive_cone ) by A; :: thesis: verum