theorem Th33: :: BCIALG_4:34

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