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