theorem :: ABSRED_0:149

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