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
take y ; :: according to ABSRED_0:def 23 :: thesis: ( x =01=> y & y <=01= y )
thus ( x =01=> y & y =01=> y ) by A1; :: thesis: verum