:: deftheorem defines <= BCIALG_1:def 11 :
for IT being non empty BCIStr_0
for x, y being Element of IT holds
( x <= y iff x \ y = 0. IT );