:: deftheorem Def14 defines being_SB-4 BCIALG_4:def 14 :
for IT being non empty BCIStr_1 holds
( IT is being_SB-4 iff for x, y being Element of IT holds (x \ y) * y = x * y );