theorem lemP: :: REALALG3:3

for R being non degenerated preordered Ring
for P being Preordering of R holds
( P + (P ^+) c= P ^+ & (P ^+) + P c= P ^+ )