theorem Lm11: :: ABSRED_0:143

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