:: deftheorem defines being_Iseki BCIALG_3:def 8 :
for IT being BCK-algebra
for a being Element of IT holds
( a is being_Iseki iff for x being Element of IT holds
( x \ a = 0. IT & a \ x = a ) );