let R be preordered Ring; :: thesis: 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; :: thesis: for a, b being Element of R st a <= P,b & b <= P,a holds
a = b
let a, b be Element of R; :: thesis: ( a <= P,b & b <= P,a implies a = b )
assume ( a <= P,b & b <= P,a ) ; :: thesis: a = b
then ( a <=_ OrdRel P,b & b <=_ OrdRel P,a ) ;
hence a = b by REALALG1:2; :: thesis: verum