for X being ARS
for x, y being Element of X holds
( not x <=01=> y or x <=01= y or x ==> y )