let R be preordered domRing; :: thesis: for P being Preordering of R
for a, b being b₁ -ordered Element of R holds abs (P,(a + b)) <= P,(abs (P,a)) + (abs (P,b))
let P be Preordering of R; :: thesis: for a, b being P -ordered Element of R holds abs (P,(a + b)) <= P,(abs (P,a)) + (abs (P,b))
let a, b be P -ordered Element of R; :: thesis: abs (P,(a + b)) <= P,(abs (P,a)) + (abs (P,b))
A1: 0. R <= P, abs (P,b) by av0;
(0. R) + (abs (P,b)) <= P,(abs (P,a)) + (abs (P,b)) by c4, av0;
then A: 0. R <= P,(abs (P,a)) + (abs (P,b)) by c3, A1;

per cases ( not a + b is P -ordered or a + b is P -ordered ) ;

suppose not a + b is P -ordered ; :: thesis: abs (P,(a + b)) <= P,(abs (P,a)) + (abs (P,b))

then ( not a + b in P & not a + b in - P ) by XBOOLE_0:def 3;
then B: abs (P,(a + b)) = - (1. R) by defa;
- (1. R) < P, 0. R by c20;
hence abs (P,(a + b)) <= P,(abs (P,a)) + (abs (P,b)) by B, A, c3; :: thesis: verum

end;

suppose AS1: a + b is P -ordered ; :: thesis: abs (P,(a + b)) <= P,(abs (P,a)) + (abs (P,b))

now :: thesis: not (abs (P,a)) + (abs (P,b)) is P -negative

assume (abs (P,a)) + (abs (P,b)) is P -negative ; :: thesis: contradiction
then - (0. R) < P, - ((abs (P,a)) + (abs (P,b))) by x2, c10;
then (0. R) + ((abs (P,a)) + (abs (P,b))) < P,(- ((abs (P,a)) + (abs (P,b)))) + ((abs (P,a)) + (abs (P,b))) by c4, RLVECT_1:8;
then (0. R) + (0. R) < P,((abs (P,a)) + (abs (P,b))) + (- ((abs (P,a)) + (abs (P,b)))) by A, c2, c3;
hence contradiction by RLVECT_1:5; :: thesis: verum

end;

then A1: ( (abs (P,a)) + (abs (P,b)) is P -ordered & not (abs (P,a)) + (abs (P,b)) is P -negative ) by A, XBOOLE_0:def 3;
B: - ((abs (P,a)) + (abs (P,b))) <= P,a + b

proof

- (abs (P,a)) <= P,a by ineq2;
then (- (abs (P,a))) + (- (abs (P,b))) <= P,a + (- (abs (P,b))) by c4;
then B1: - ((abs (P,a)) + (abs (P,b))) <= P,a + (- (abs (P,b))) by RLVECT_1:31;
- (abs (P,b)) <= P,b by ineq2;
then a + (- (abs (P,b))) <= P,a + b by c4;
hence - ((abs (P,a)) + (abs (P,b))) <= P,a + b by B1, c3; :: thesis: verum

end;

B1: a + (abs (P,b)) <= P,(abs (P,a)) + (abs (P,b)) by c4, ineq2;
a + b <= P,(abs (P,a)) + (abs (P,b))

proof

a + b <= P,(abs (P,b)) + a by c4, ineq2;
hence a + b <= P,(abs (P,a)) + (abs (P,b)) by B1, c3; :: thesis: verum

end;

hence abs (P,(a + b)) <= P,(abs (P,a)) + (abs (P,b)) by AS1, A1, B, ineq1; :: thesis: verum

end;

end;