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