theorem sq1: :: REALALG2:80

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 )