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, Th3; :: thesis: verum