let R be ordered domRing; for O being Ordering of R
for a, b being non b1 -negative Element of R holds
( a <= O,b iff a ^2 <= O,b ^2 )
let P be Ordering of R; 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; ( 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;