theorem :: ABSRED_0:26

for X being ARS
for x, y, z being Element of X st x ==> y & y ==> z holds
x =+=> z by Th2;