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