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