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 22 :: thesis: x <<>> y
take z ; :: according to ABSRED_0:def 20 :: thesis: ( x <=*= z & z =*=> y )
thus ( x <=*= z & z =*=> y ) by A2, Lem1; :: thesis: verum