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

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

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

hence x >>01<< y ; :: thesis: verum

end;

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

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

end;

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

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

end;

end;