let R be preordered Ring; :: thesis: for P being Preordering of R
for a, b, c being Element of R st a <= P,b & 0. R <= P,c holds
a * c <= P,b * c
let P be Preordering of R; :: thesis: for a, b, c being Element of R st a <= P,b & 0. R <= P,c holds
a * c <= P,b * c
let a, b, c be Element of R; :: thesis: ( a <= P,b & 0. R <= P,c implies a * c <= P,b * c )
assume ( a <= P,b & 0. R <= P,c ) ; :: thesis: a * c <= P,b * c
then ( a <=_ OrdRel P,b & 0. R <=_ OrdRel P,c ) ;
hence a * c <= P,b * c by lemOP, REALALG1:def 4; :: thesis: verum