theorem Th7: :: ABSRED_0:7

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