:: deftheorem Def8 defines being_BCK-5 BCIALG_1:def 8 :
for IT being non empty BCIStr_0 holds
( IT is being_BCK-5 iff for x being Element of IT holds x ` = 0. IT );