let R be preordered domRing; for P being Preordering of R
for a, b, c being Element of R st a < P,b & c < P, 0. R holds
b * c < P,a * c
let P be Preordering of R; for a, b, c being Element of R st a < P,b & c < P, 0. R holds
b * c < P,a * c
let a, b, c be Element of R; ( a < P,b & c < P, 0. R implies b * c < P,a * c )
assume AS:
( a < P,b & c < P, 0. R )
; b * c < P,a * c
then
- (0. R) < P, - c
by c10a, RLVECT_1:18;
then A:
a * (- c) < P,b * (- c)
by AS, c5, GCD_1:1;
B: - (b * (- c)) =
(- b) * (- c)
by VECTSP_1:9
.=
b * c
by VECTSP_1:10
;
- (a * (- c)) =
(- a) * (- c)
by VECTSP_1:9
.=
a * c
by VECTSP_1:10
;
hence
b * c < P,a * c
by A, B, c10a, RLVECT_1:18; verum