theorem Th3: :: ABSRED_0:3

for X being ARS
for x, y, z being Element of X st x =*=> y & y =*=> z holds
x =*=> z by REWRITE1:16;