theorem Th23: :: BCIALG_3:23

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 \ (a \ y) = y \ (a \ x) )