let X be ARS ; :: thesis: for x, y being Element of X st ( x <== y or x = y or x ==> y ) holds
x <=01=> y
let x, y be Element of X; :: thesis: ( ( x <== y or x = y or x ==> y ) implies x <=01=> y )
assume A1: ( x <== y or x = y or x ==> y ) ; :: thesis: x <=01=> y
A2: ( x <==> y or x = y ) by A1;
thus x <=01=> y by A2; :: thesis: verum