theorem :: ABSRED_0:126

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