let R be preordered Ring; :: thesis: for P being Preordering of R
for a, b, c being Element of R st a <= P,b 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 holds
a + c <= P,b + c
let a, b, c be Element of R; :: thesis: ( a <= P,b implies a + c <= P,b + c )
assume a <= P,b ; :: thesis: a + c <= P,b + c
then a <=_ OrdRel P,b ;
hence a + c <= P,b + c by lemOP, REALALG1:def 3; :: thesis: verum