theorem :: ABSRED_0:53

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