let X be BCI-algebra; :: thesis: for x being Element of X holds x \ (0. X) = x
let x be Element of X; :: thesis: x \ (0. X) = x
(x \ (x \ (0. X))) \ (0. X) = 0. X by Th1;
then A1: x \ (x \ (0. X)) = 0. X by Lm1;
0. X = (x \ (x \ x)) \ x by Th1
.= (x \ (0. X)) \ x by Def5 ;
hence x \ (0. X) = x by A1, Def7; :: thesis: verum