:: deftheorem Def7 defines being_BCI-4 BCIALG_1:def 7 :
for IT being non empty BCIStr_0 holds
( IT is being_BCI-4 iff for x, y being Element of IT st x \ y = 0. IT & y \ x = 0. IT holds
x = y );