theorem sq5: :: REALALG2:83

for R being preordered Ring
for P being Preordering of R
for a being Element of R st a in (- P) \ {(0. R)} holds
not a is square