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