let R be preordered domRing; :: thesis: 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; :: thesis: 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; :: thesis: ( a < P,b & c < P, 0. R implies b * c < P,a * c )
assume AS: ( a < P,b & c < P, 0. R ) ; :: thesis: 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; :: thesis: verum