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