let O be Ordering of F_Real; :: thesis: O = Positives(F_Real)
X: QS F_Real c= O by ord2;

now :: thesis: for x being object st x in Positives(F_Real) holds
x in O

let x be object ; :: thesis: ( x in Positives(F_Real) implies x in O )
assume x in Positives(F_Real) ; :: thesis: x in O
then consider r being Element of F_Real such that
A: ( x = r & 0 <= r ) ;
reconsider q = sqrt r as Element of F_Real by XREAL_0:def 1;
r = (sqrt r) ^2 by A, SQUARE_1:def 2
.= q ^2 ;
then r is square ;
then r in QS F_Real ;
hence x in O by A, X; :: thesis: verum

end;

then Positives(F_Real) c= O ;
hence O = Positives(F_Real) by ordsub; :: thesis: verum