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

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