:: deftheorem Def8 defines <=+=> ABSRED_0:def 8 :
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 ) );