let R be preordered domRing; :: thesis: for P being Preordering of R
for a being b₁ -ordered Element of R
for p being b₁ -ordered non b₁ -negative Element of R holds
( abs (P,a) <= P,p iff ( - p <= P,a & a <= P,p ) )
let P be Preordering of R; :: thesis: for a being P -ordered Element of R
for p being P -ordered non P -negative Element of R holds
( abs (P,a) <= P,p iff ( - p <= P,a & a <= P,p ) )
let a be P -ordered Element of R; :: thesis: for p being P -ordered non P -negative Element of R holds
( abs (P,a) <= P,p iff ( - p <= P,a & a <= P,p ) )
let p be P -ordered non P -negative Element of R; :: thesis: ( abs (P,a) <= P,p iff ( - p <= P,a & a <= P,p ) )
H: ( not p in (- P) \ {(0. R)} & p in P \/ (- P) ) by defn, defppp;
then ( not p in - P or p in {(0. R)} ) by XBOOLE_0:def 5;
then As: ( not p in - P or p = 0. R ) by TARSKI:def 1;
then AS: ( a in P \/ (- P) & 0. R <= P,p ) by defppp, H, XBOOLE_0:def 3, REALALG1:25;

hereby :: thesis: ( - p <= P,a & a <= P,p implies abs (P,a) <= P,p )

assume A1: abs (P,a) <= P,p ; :: thesis: ( - p <= P,a & a <= P,p )

per cases ( a in P or a in - P ) by AS, XBOOLE_0:def 3;

suppose a in P ; :: thesis: ( - p <= P,a & a <= P,p )

then A2: 0. R <= P,a ;
A3: a <= P, abs (P,a) by ineq2;
- p <= P, 0. R by As, H, XBOOLE_0:def 3, REALALG1:25;
hence ( - p <= P,a & a <= P,p ) by A3, A2, A1, c3; :: thesis: verum

end;

suppose a in - P ; :: thesis: ( - p <= P,a & a <= P,p )

then - a in - (- P) ;
then A3: - (- a) <= P, 0. R ;
- (abs (P,a)) <= P,a by ineq2;
then - a <= P, - (- (abs (P,a))) by c10a;
then - a <= P,p by A1, c3;
hence ( - p <= P,a & a <= P,p ) by A3, AS, c3, c10a; :: thesis: verum

end;

end;

end;

assume A1: ( - p <= P,a & a <= P,p ) ; :: thesis: abs (P,a) <= P,p

per cases ( a in P or a in - P ) by AS, XBOOLE_0:def 3;

suppose a in P ; :: thesis: abs (P,a) <= P,p

then 0. R <= P,a ;
hence abs (P,a) <= P,p by A1, av2; :: thesis: verum

end;

suppose a in - P ; :: thesis: abs (P,a) <= P,p

then - a in - (- P) ;
then - (- a) <= P, 0. R ;
then abs (P,a) = - a by av3;
hence abs (P,a) <= P,p by A1, c10a; :: thesis: verum

end;

end;