theorem ineq2: :: REALALG2:75

for R being non degenerated preordered Ring
for P being Preordering of R
for a being Element of R holds
( ( - (abs (P,a)) <= P,a & a <= P, abs (P,a) ) iff a is P -ordered )