let X be ARS ; :: thesis: for x, y, z being Element of X st x >><< z & z <== y holds
x >><< y
let x, y, z be Element of X; :: thesis: ( x >><< z & z <== y implies x >><< y )
given u being Element of X such that A3: ( x =*=> u & u <=*= z ) ; :: according to ABSRED_0:def 21 :: thesis: ( not z <== y or x >><< y )
assume A2: z <== y ; :: thesis: x >><< y
take u ; :: according to ABSRED_0:def 21 :: thesis: ( x =*=> u & u <=*= y )
thus x =*=> u by A3; :: thesis: u <=*= y
thus y =*=> u by A2, A3, Lem5; :: thesis: verum