theorem Th8: :: BCIALG_4:9

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