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