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