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

( (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