theorem :: REALALG2:81
for R being ordered domRing
for O being Ordering of R
for a, b being non b2 -negative Element of R holds
( a < O,b iff a ^2 < O,b ^2 )