let X be BCI-Algebra_with_Condition(S); :: thesis: (0. X) |^ 2 = 0. X
(0. X) * (0. X) = ((0. X) * (0. X)) \ (0. X) by BCIALG_1:2;
then (0. X) * (0. X) <= 0. X by Lm2;
then A1: ((0. X) * (0. X)) \ (0. X) = 0. X ;
0. X <= (0. X) * ((0. X) \ (0. X)) by Th12;
then 0. X <= (0. X) * (0. X) by BCIALG_1:def 5;
then (0. X) \ ((0. X) * (0. X)) = 0. X ;
then (0. X) * (0. X) = 0. X by A1, BCIALG_1:def 7;
hence (0. X) |^ 2 = 0. X by Th22; :: thesis: verum