let X be BCI-Algebra_with_Condition(S); :: thesis: for x being Element of X holds
( (0. X) * x = x & x * (0. X) = x )
let x be Element of X; :: thesis: ( (0. X) * x = x & x * (0. X) = x )
(x \ (0. X)) \ x = (x \ x) \ (0. X) by BCIALG_1:7
.= (0. X) \ (0. X) by BCIALG_1:def 5
.= 0. X by BCIALG_1:def 5 ;
then x \ (0. X) <= x ;
then x <= (0. X) * x by Lm2;
then A1: x \ ((0. X) * x) = 0. X ;
((0. X) * x) \ (0. X) <= x by Lm2;
then (0. X) * x <= x by BCIALG_1:2;
then ((0. X) * x) \ x = 0. X ;
then (0. X) * x = x by A1, BCIALG_1:def 7;
hence ( (0. X) * x = x & x * (0. X) = x ) by Th6; :: thesis: verum