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

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