theorem v1a: :: REALALG2:16
for R being preordered Ring
for P being Preordering of R holds (- P) * P = P * (- P)