let F be ordered Field; :: thesis: for P being Ordering of F
for E being Field st E == F holds
( E is ordered & ex Q being Subset of E st
( Q = P & Q is positive_cone ) )
let P be Ordering of F; :: thesis: for E being Field st E == F holds
( E is ordered & ex Q being Subset of E st
( Q = P & Q is positive_cone ) )
let E be Field; :: thesis: ( E == F implies ( E is ordered & ex Q being Subset of E st
( Q = P & Q is positive_cone ) ) )
assume AS: E == F ; :: thesis: ( E is ordered & ex Q being Subset of E st
( Q = P & Q is positive_cone ) )
then A: E is Subring of F by FIELD_5:12;
hence E is ordered ; :: thesis: ex Q being Subset of E st
( Q = P & Q is positive_cone )
reconsider K = E as ordered Field by A;
P /\ the carrier of K is Ordering of K by A, REALALG1:34;
hence ex Q being Subset of E st
( Q = P & Q is positive_cone ) by AS, XBOOLE_1:28; :: thesis: verum