:: deftheorem defines Iseki_extension BCIALG_3:def 9 :
for IT being BCK-algebra holds
( IT is Iseki_extension iff ex a being Element of IT st a is being_Iseki );