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