let R be preordered Ring; :: thesis: for P being Preordering of R
for a, b being Element of R holds
( a <= P,b iff a <=_ OrdRel P,b )
let P be Preordering of R; :: thesis: for a, b being Element of R holds
( a <= P,b iff a <=_ OrdRel P,b )
let a, b be Element of R; :: thesis: ( a <= P,b iff a <=_ OrdRel P,b )
now :: thesis: ( a <=_ OrdRel P,b implies a <= P,b )
assume a <=_ OrdRel P,b ; :: thesis: a <= P,b
then consider a1, b1 being Element of R such that
H: ( [a,b] = [a1,b1] & a1 <= P,b1 ) ;
( a = a1 & b = b1 ) by H, XTUPLE_0:1;
hence a <= P,b by H; :: thesis: verum
end;
hence ( a <= P,b iff a <=_ OrdRel P,b ) ; :: thesis: verum