let F be ordered Field; :: thesis: 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) )
let E be FieldExtension of F; :: thesis: for P being Ordering of F holds
( QS (E,P) is prepositive_cone iff not - (1. E) in QS (E,P) )
let P be Ordering of F; :: thesis: ( QS (E,P) is prepositive_cone iff not - (1. E) in QS (E,P) )
set T = QS (E,P);

A: now :: thesis: ( QS (E,P) is prepositive_cone implies not - (1. E) in QS (E,P) )

assume AS: QS (E,P) is prepositive_cone ; :: thesis: not - (1. E) in QS (E,P)
then reconsider E1 = E as preordered Field by REALALG1:def 16;
reconsider O = QS (E,P) as Preordering of E1 by AS;
not - (1. E) in O by REALALG1:26;
hence not - (1. E) in QS (E,P) ; :: thesis: verum

end;

now :: thesis: ( not - (1. E) in QS (E,P) implies QS (E,P) is prepositive_cone )

assume AS: not - (1. E) in QS (E,P) ; :: thesis: QS (E,P) is prepositive_cone
( QS E c= QS (E,P) & SQ E c= QS E ) by REALALG1:def 13, REALALG1:18;
then A: SQ E c= QS (E,P) ;
(QS (E,P)) * (QS (E,P)) c= QS (E,P)

proof

now :: thesis: for o being object st o in (QS (E,P)) * (QS (E,P)) holds
o in QS (E,P)

let o be object ; :: thesis: ( o in (QS (E,P)) * (QS (E,P)) implies o in QS (E,P) )
assume o in (QS (E,P)) * (QS (E,P)) ; :: thesis: o in QS (E,P)
then consider a, b being Element of E such that
C: ( o = a * b & a in QS (E,P) & b in QS (E,P) ) ;
thus o in QS (E,P) by C, REALALG1:def 5; :: thesis: verum

end;

hence (QS (E,P)) * (QS (E,P)) c= QS (E,P) ; :: thesis: verum

end;

then QS (E,P) is negative-disjoint by A, AS, REALALG1:21;
hence QS (E,P) is prepositive_cone ; :: thesis: verum

end;

hence ( QS (E,P) is prepositive_cone iff not - (1. E) in QS (E,P) ) by A; :: thesis: verum