theorem Th6: :: BCIALG_4:7

for X being BCI-Algebra_with_Condition(S)
for x, y being Element of X holds x * y = y * x