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

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