theorem :: BCIALG_4:36

for X being BCI-Algebra_with_Condition(S)
for x, a1, a2, a3 being Element of X holds ((x \ a1) \ a2) \ a3 = x \ (Product_S <*a1,a2,a3*>)