let X be ARS ; :: thesis: for x, y, z being Element of X st x ==> y & z ==> y holds

x >>01<< z

let x, y, z be Element of X; :: thesis: ( x ==> y & z ==> y implies x >>01<< z )

assume A1: x ==> y ; :: thesis: ( not z ==> y or x >>01<< z )

assume A2: z ==> y ; :: thesis: x >>01<< z

take y ; :: according to ABSRED_0:def 23 :: thesis: ( x =01=> y & y <=01= z )

thus y <=01= x by A1; :: thesis: y <=01= z

thus z =01=> y by A2; :: thesis: verum

x >>01<< z

let x, y, z be Element of X; :: thesis: ( x ==> y & z ==> y implies x >>01<< z )

assume A1: x ==> y ; :: thesis: ( not z ==> y or x >>01<< z )

assume A2: z ==> y ; :: thesis: x >>01<< z

take y ; :: according to ABSRED_0:def 23 :: thesis: ( x =01=> y & y <=01= z )

thus y <=01= x by A1; :: thesis: y <=01= z

thus z =01=> y by A2; :: thesis: verum