let R be ordered Ring; :: thesis: for O being Ordering of R
for a, b being Element of R holds
( a <= O,b or b <= O,a )
let O be Ordering of R; :: thesis: for a, b being Element of R holds
( a <= O,b or b <= O,a )
let a, b be Element of R; :: thesis: ( a <= O,b or b <= O,a )
X: O \/ (- O) = the carrier of R by REALALG1:def 8;
assume not a <= O,b ; :: thesis: b <= O,a
then b - a in - O by X, XBOOLE_0:def 3;
then - (b - a) in - (- O) ;
hence b <= O,a by RLVECT_1:33; :: thesis: verum