theorem :: BCIALG_4:35

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