let R be preordered Ring; 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; for a, b being Element of R holds
( a <= P,b iff - b <= P, - a )
let a, b be Element of R; ( a <= P,b iff - b <= P, - a )
(- a) - (- b) = (- a) + b
;
hence
( a <= P,b iff - b <= P, - a )
; verum