theorem Lem3: :: ABSRED_0:12

for X being ARS
for x, y, z being Element of X st x ==> y & y ==> z holds
x =*=> z