let R be preordered Ring; :: thesis: for P being Preordering of R
for a being Element of R holds a <= P,a
let P be Preordering of R; :: thesis: for a being Element of R holds a <= P,a
let a be Element of R; :: thesis: a <= P,a
a <=_ OrdRel P,a by REALALG1:1;
hence a <= P,a by lemOP; :: thesis: verum