:: deftheorem Def5 defines being_I BCIALG_1:def 5 :
for IT being non empty BCIStr_0 holds
( IT is being_I iff for x being Element of IT holds x \ x = 0. IT );