:: deftheorem defines involutory BCIALG_3:def 7 :
for IT being bounded BCK-algebra holds
( IT is involutory iff for a being Element of IT st a is being_greatest holds
for x being Element of IT holds a \ (a \ x) = x );