:: deftheorem defines bounded BCIALG_3:def 6 :
for IT being BCK-algebra holds
( IT is bounded iff ex a being Element of IT st a is being_greatest );