theorem :: ABSRED_0:5

for X being ARS
for x, y being Element of X holds
( x <==> y iff [x,y] in the reduction of X \/ ( the reduction of X ~) )