let R be non degenerated preordered Ring; for P being Preordering of R
for a being Element of R holds
( ( - (abs (P,a)) <= P,a & a <= P, abs (P,a) ) iff a is P -ordered )
let P be Preordering of R; for a being Element of R holds
( ( - (abs (P,a)) <= P,a & a <= P, abs (P,a) ) iff a is P -ordered )
let a be Element of R; ( ( - (abs (P,a)) <= P,a & a <= P, abs (P,a) ) iff a is P -ordered )
hereby ( a is P -ordered implies ( - (abs (P,a)) <= P,a & a <= P, abs (P,a) ) )
assume AS:
(
- (abs (P,a)) <= P,
a &
a <= P,
abs (
P,
a) )
;
a is P -ordered now a is P -ordered assume
not
a is
P -ordered
;
contradictionthen B:
(
- (- (1. R)) <= P,
a &
a <= P,
- (1. R) )
by AS, av00;
(
0. R < P,
1. R &
- (1. R) < P,
0. R )
by c20;
then
- (1. R) < P,
1. R
by c2, c3;
then
a < P,
1. R
by B, c2, c3;
hence
contradiction
by B, c2;
verum end; hence
a is
P -ordered
;
verum
end;
X:
P + P c= P
by REALALG1:def 14;
hence
( a is P -ordered implies ( - (abs (P,a)) <= P,a & a <= P, abs (P,a) ) )
; verum