for X being ARS
for x, y being Element of X holds
( x >>01<< y iff x,y are_convergent<=1_wrt the reduction of X )