reconsider b = sqrt 2 as Element of F_Real by XREAL_0:def 1;
b ^2 = (sqrt 2) ^2 ;
hence 2. F_Real is square by SQUARE_1:def 2; :: thesis: verum