let X be ARS ; :: thesis: for x, y being Element of X st x >>01<< y holds

x >><< y

let x, y be Element of X; :: thesis: ( x >>01<< y implies x >><< y )

given z being Element of X such that A2: ( x =01=> z & z <=01= y ) ; :: according to ABSRED_0:def 23 :: thesis: x >><< y

take z ; :: according to ABSRED_0:def 21 :: thesis: ( x =*=> z & z <=*= y )

thus ( x =*=> z & z <=*= y ) by A2, Lem1; :: thesis: verum

x >><< y

let x, y be Element of X; :: thesis: ( x >>01<< y implies x >><< y )

given z being Element of X such that A2: ( x =01=> z & z <=01= y ) ; :: according to ABSRED_0:def 23 :: thesis: x >><< y

take z ; :: according to ABSRED_0:def 21 :: thesis: ( x =*=> z & z <=*= y )

thus ( x =*=> z & z <=*= y ) by A2, Lem1; :: thesis: verum