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

per cases ( x ==> y or x <== y ) by A1;

suppose A2: x ==> y ; :: thesis: x <<01>> y

take x ; :: according to ABSRED_0:def 22 :: thesis: ( x <=01= x & x =01=> y )
thus ( x <=01= x & x =01=> y ) by A2; :: thesis: verum

end;

suppose A3: x <== y ; :: thesis: x <<01>> y

take y ; :: according to ABSRED_0:def 22 :: thesis: ( x <=01= y & y =01=> y )
thus ( x <=01= y & y =01=> y ) by A3; :: thesis: verum

end;

end;