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