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

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