theorem c10: :: REALALG2:53

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 ) by c10a, RLVECT_1:18;