theorem :: ABSRED_0:134

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