let R be non degenerated preordered Ring; :: thesis: for P being Preordering of R holds
( P + (P ^+) c= P ^+ & (P ^+) + P c= P ^+ )
let P be Preordering of R; :: thesis: ( P + (P ^+) c= P ^+ & (P ^+) + P c= P ^+ )
set S = P \ {(0. R)};
H: P + P c= P by REALALG1:def 14;

now :: thesis: for o being object st o in P + (P \ {(0. R)}) holds
o in P \ {(0. R)}

let o be object ; :: thesis: ( o in P + (P \ {(0. R)}) implies o in P \ {(0. R)} )
assume o in P + (P \ {(0. R)}) ; :: thesis: o in P \ {(0. R)}
then consider a, b being Element of R such that
A: ( o = a + b & a in P & b in P \ {(0. R)} ) ;
B: ( b in P & not b in {(0. R)} ) by A, XBOOLE_0:def 5;
then C: a + b in P + P by A;

now :: thesis: not a + b in {(0. R)}

assume a + b in {(0. R)} ; :: thesis: contradiction
then a + b = 0. R by TARSKI:def 1;
then a = - b by RLVECT_1:6;
then - (- b) in - P by A;
then b in P /\ (- P) by B;
hence contradiction by B, REALALG1:def 7; :: thesis: verum

end;

hence o in P \ {(0. R)} by C, A, H, XBOOLE_0:def 5; :: thesis: verum

end;

hence P + (P ^+) c= P ^+ ; :: thesis: (P ^+) + P c= P ^+

now :: thesis: for o being object st o in (P \ {(0. R)}) + P holds
o in P \ {(0. R)}

let o be object ; :: thesis: ( o in (P \ {(0. R)}) + P implies o in P \ {(0. R)} )
assume o in (P \ {(0. R)}) + P ; :: thesis: o in P \ {(0. R)}
then consider a, b being Element of R such that
A: ( o = a + b & a in P \ {(0. R)} & b in P ) ;
B: ( a in P & not a in {(0. R)} ) by A, XBOOLE_0:def 5;
then C: a + b in P + P by A;

now :: thesis: not a + b in {(0. R)}

assume a + b in {(0. R)} ; :: thesis: contradiction
then a + b = 0. R by TARSKI:def 1;
then b = - a by RLVECT_1:6;
then - (- a) in - P by A;
then a in P /\ (- P) by B;
hence contradiction by B, REALALG1:def 7; :: thesis: verum

end;

hence o in P \ {(0. R)} by C, A, H, XBOOLE_0:def 5; :: thesis: verum

end;

hence (P ^+) + P c= P ^+ ; :: thesis: verum