theorem Th22: :: BCIALG_3:22

for X being bounded BCK-algebra holds
( X is involutory iff for a being Element of X st a is being_greatest holds
for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) )