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

(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