theorem v1: :: REALALG2:17

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