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 is P -ordered & b is P -ordered ) ;
then AS: ( 0. R <= P,a & 0. R <= P,b ) by x1a;

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

assume K: a < P,b ; :: thesis: a ^2 < P,b ^2
( a is Sqrt of a ^2 & b is Sqrt of b ^2 ) by defsqrt;
hence a ^2 < P,b ^2 by K, AS, sq1, sq0; :: thesis: verum

end;

thus ( a ^2 < P,b ^2 implies a < P,b ) by sq1; :: thesis: verum