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