theorem :: BCIALG_4:26

for n being Nat
for X being BCI-Algebra_with_Condition(S) holds (0. X) |^ n = 0. X