:: deftheorem Def13 defines being_SB-2 BCIALG_4:def 13 :
for IT being non empty BCIStr_1 holds
( IT is being_SB-2 iff for x, y being Element of IT holds x * y = y * x );