theorem :: ABSRED_0:137

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