theorem Lm8: :: ABSRED_0:47

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