theorem :: ABSRED_0:140

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