theorem :: BCIALG_4:41

for X being BCK-Algebra_with_Condition(S)
for x being Element of X holds (x \ (0. X)) * ((0. X) \ x) = x