let R be ordered domRing; :: thesis: for O being Ordering of R
for a, b being non b₁ -negative Element of R holds
( a <= O,b iff a ^2 <= O,b ^2 )
let P be Ordering of R; :: thesis: for a, b being non P -negative Element of R holds
( a <= P,b iff a ^2 <= P,b ^2 )
let a, b be non P -negative Element of R; :: thesis: ( a <= P,b iff a ^2 <= P,b ^2 )
the carrier of R = P \/ (- P) by REALALG1:def 8;
then A: ( a is P -ordered & b is P -ordered ) ;
then AS: ( 0. R <= P,a & 0. R <= P,b ) by x1a;

per cases ( a = 0. R or a <> 0. R ) ;

suppose K: a = 0. R ; :: thesis: ( a <= P,b iff a ^2 <= P,b ^2 )

( SQ R c= P & b ^2 in SQ R ) by REALALG1:def 14;
hence ( a <= P,b iff a ^2 <= P,b ^2 ) by A, x1a, K; :: thesis: verum

end;

suppose K: a <> 0. R ; :: thesis: ( a <= P,b iff a ^2 <= P,b ^2 )

hereby :: thesis: ( a ^2 <= P,b ^2 implies a <= P,b )

assume a <= P,b ; :: thesis: a ^2 <= P,b ^2
then ( a * a <= P,b * a & a * b <= P,b * b ) by AS, c5;
hence a ^2 <= P,b ^2 by c3; :: thesis: verum

end;

C: ( P * (- P) c= - P & P + P c= P ) by v2, REALALG1:def 14;
B: a + b in P + P by AS;
D: the carrier of R = P \/ (- P) by REALALG1:def 8;
assume a ^2 <= P,b ^2 ; :: thesis: a <= P,b
then A: (b + a) * (b - a) in P by P4a;

per cases ( b - a in - P or b - a in P ) by D, XBOOLE_0:def 3;

suppose b - a in - P ; :: thesis: a <= P,b

then (b + a) * (b - a) in P * (- P) by B, C;
then (b + a) * (b - a) in P /\ (- P) by A, C;
then (b + a) * (b - a) in {(0. R)} by REALALG1:def 7;
then D: (b + a) * (b - a) = 0. R by TARSKI:def 1;

per cases ( b + a = 0. R or b - a = 0. R ) by D, VECTSP_2:def 1;

suppose b + a = 0. R ; :: thesis: a <= P,b

then a = - b by RLVECT_1:6;
then a in - P by AS;
then a in P /\ (- P) by AS;
then a in {(0. R)} by REALALG1:def 7;
hence a <= P,b by K, TARSKI:def 1; :: thesis: verum

end;

suppose b - a = 0. R ; :: thesis: a <= P,b

hence a <= P,b by REALALG1:25; :: thesis: verum

end;

end;

end;

suppose b - a in P ; :: thesis: a <= P,b

hence a <= P,b ; :: thesis: verum

end;

end;

end;

end;