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