theorem Th6: :: ABSRED_0:6

for X being ARS
for x, y being Element of X st x <==> y holds
x <=*=> y