theorem c10a: :: REALALG2:42
for R being preordered Ring
for P being Preordering of R
for a, b being Element of R holds
( a <= P,b iff - b <= P, - a )