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