theorem :: REALALG2:81

for R being ordered domRing
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 )