let X be non empty BCIStr_0 ; :: thesis: ( X is implicative BCI-algebra iff for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & (x \ (x \ y)) \ (y \ x) = y \ (y \ x) ) )
thus ( X is implicative BCI-algebra implies for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & (x \ (x \ y)) \ (y \ x) = y \ (y \ x) ) ) by Def24, Th1, Th2; :: thesis: ( ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & (x \ (x \ y)) \ (y \ x) = y \ (y \ x) ) ) implies X is implicative BCI-algebra )
thus ( ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & (x \ (x \ y)) \ (y \ x) = y \ (y \ x) ) ) implies X is implicative BCI-algebra ) :: thesis: verum

proof

assume A1: for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & (x \ (x \ y)) \ (y \ x) = y \ (y \ x) ) ; :: thesis: X is implicative BCI-algebra

A2: now :: thesis: for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X )

let x, y, z be Element of X; :: thesis: ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X )
thus ((x \ y) \ (x \ z)) \ (z \ y) = 0. X by A1; :: thesis: (x \ (x \ y)) \ y = 0. X
(x \ (x \ y)) \ y = ((x \ (0. X)) \ (x \ y)) \ y by A1
.= ((x \ (0. X)) \ (x \ y)) \ (y \ (0. X)) by A1 ;
hence (x \ (x \ y)) \ y = 0. X by A1; :: thesis: verum

end;

now :: thesis: for x, y being Element of X st x \ y = 0. X & y \ x = 0. X holds
x = y

let x, y be Element of X; :: thesis: ( x \ y = 0. X & y \ x = 0. X implies x = y )
assume that
A3: x \ y = 0. X and
A4: y \ x = 0. X ; :: thesis: x = y
x = x \ (0. X) by A1
.= (y \ (y \ x)) \ (x \ y) by A1, A3
.= y \ (0. X) by A1, A3, A4 ;
hence x = y by A1; :: thesis: verum

end;

then A5: X is being_BCI-4 ;

now :: thesis: for x being Element of X holds x \ x = 0. X

let x be Element of X; :: thesis: x \ x = 0. X
x \ x = (x \ (0. X)) \ x by A1
.= (x \ (0. X)) \ (x \ (0. X)) by A1
.= ((x \ (0. X)) \ (x \ (0. X))) \ (0. X) by A1
.= ((x \ (0. X)) \ (x \ (0. X))) \ ((0. X) `) by A1 ;
hence x \ x = 0. X by A1; :: thesis: verum

end;

then X is being_I ;
hence X is implicative BCI-algebra by A1, A5, A2, Def24, Th1; :: thesis: verum

end;