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