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

( 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