theorem v2: :: REALALG2:18

for R being preordered Ring
for P being Preordering of R holds
( (- P) * P c= - P & P * (- P) c= - P )