theorem Th24: :: BCIALG_4:25

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