set R = F_Real ;
set P = the Ordering of F_Real;
A: - (1. F_Real) in - the Ordering of F_Real by REALALG1:14, REALALG1:25;
not - (1. F_Real) in {(0. F_Real)} ;
then - (1. F_Real) in (- the Ordering of F_Real) \ {(0. F_Real)} by A, XBOOLE_0:def 5;
hence not - (1. F_Real) is being_a_square by REALALG2:83; :: thesis: verum