:: deftheorem defines =*=> ABSRED_0:def 3 :
for X being ARS
for x, y being Element of X holds
( x =*=> y iff the reduction of X reduces x,y );