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