theorem :: BCIALG_4:43

for X being commutative BCK-Algebra_with_Condition(S)
for a being Element of X st a is greatest holds
for x, y being Element of X holds x * y = a \ ((a \ x) \ y)