:: deftheorem defines =+=> ABSRED_0:def 4 :
for X being ARS
for x, y being Element of X holds
( x =+=> y iff ex z being Element of X st
( x ==> z & z =*=> y ) );