let R be preordered Ring; :: thesis: for P being Preordering of R
for a, b being Element of R holds
( a <= P,b iff - b <= P, - a )
let P be Preordering of R; :: thesis: for a, b being Element of R holds
( a <= P,b iff - b <= P, - a )
let a, b be Element of R; :: thesis: ( a <= P,b iff - b <= P, - a )
(- a) - (- b) = (- a) + b ;
hence ( a <= P,b iff - b <= P, - a ) ; :: thesis: verum