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