let R be preordered Ring; :: 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 ;
then A: a * (- c) <= P,b * (- c) by AS, c5;
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; :: thesis: verum