:: deftheorem Def3 defines being_B BCIALG_1:def 3 :
for IT being non empty BCIStr_0 holds
( IT is being_B iff for x, y, z being Element of IT holds ((x \ y) \ (z \ y)) \ (x \ z) = 0. IT );