let X be ARS ; :: thesis: for x, y, z being Element of X st x ==> y & x ==> z holds
y <<01>> z
let x, y, z be Element of X; :: thesis: ( x ==> y & x ==> z implies y <<01>> z )
assume A1: x ==> y ; :: thesis: ( not x ==> z or y <<01>> z )
assume A2: x ==> z ; :: thesis: y <<01>> z
take x ; :: according to ABSRED_0:def 22 :: thesis: ( y <=01= x & x =01=> z )
thus y <=01= x by A1; :: thesis: x =01=> z
thus x =01=> z by A2; :: thesis: verum