theorem ord1: :: REALALG1:23

for R being preordered Ring
for P being Preordering of R
for a being Element of R holds a ^2 in P