let X be non empty BCIStr_0 ; :: thesis: ( X is BCI-algebra iff ( X is being_I & X is being_BCI-4 & ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ) ) )
thus ( X is BCI-algebra implies ( X is being_I & X is being_BCI-4 & ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ) ) ) :: thesis: ( X is being_I & X is being_BCI-4 & ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ) implies X is BCI-algebra )

proof

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

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 & x \ x = 0. X & ( x \ y = 0. X & y \ x = 0. X implies x = y ) )

let x, y, z be Element of X; :: thesis: ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X & x \ x = 0. X & ( x \ y = 0. X & y \ x = 0. X implies x = y ) )
A2: ((x \ y) \ (z \ y)) \ (x \ z) = 0. X by A1, Def3;
A3: for x, y, z being Element of X holds (x \ y) \ z = (x \ z) \ y

proof

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

end;

then (x \ (x \ y)) \ y = (x \ y) \ (x \ y) ;
hence ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X & x \ x = 0. X & ( x \ y = 0. X & y \ x = 0. X implies x = y ) ) by A1, A2, A3, Def5, Def7; :: thesis: verum

end;

hence ( X is being_I & X is being_BCI-4 & ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ) ) ; :: thesis: verum

end;

assume that
A4: X is being_I and
A5: X is being_BCI-4 and
A6: for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ; :: thesis: X is BCI-algebra
A7: for x being Element of X st x \ (0. X) = 0. X holds
x = 0. X

proof

let x be Element of X; :: thesis: ( x \ (0. X) = 0. X implies x = 0. X )
assume A8: x \ (0. X) = 0. X ; :: thesis: x = 0. X
then x ` = (x \ (x \ x)) \ x by A4
.= 0. X by A6 ;
hence x = 0. X by A5, A8; :: thesis: verum

end;

A9: for x being Element of X holds x \ (0. X) = x

proof

let x be Element of X; :: thesis: x \ (0. X) = x
(x \ (x \ (0. X))) \ (0. X) = 0. X by A6;
then A10: x \ (x \ (0. X)) = 0. X by A7;
0. X = (x \ (x \ x)) \ x by A6
.= (x \ (0. X)) \ x by A4 ;
hence x \ (0. X) = x by A5, A10; :: thesis: verum

end;

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

proof

let x, y, z be Element of X; :: thesis: ( x \ y = 0. X & y \ z = 0. X implies x \ z = 0. X )
assume that
A12: x \ y = 0. X and
A13: y \ z = 0. X ; :: thesis: x \ z = 0. X
((x \ z) \ (x \ y)) \ (y \ z) = 0. X by A6;
then (x \ z) \ (x \ y) = 0. X by A9, A13;
hence x \ z = 0. X by A9, A12; :: thesis: verum

end;

A14: for x, y, z being Element of X holds ((x \ y) \ z) \ ((x \ z) \ y) = 0. X

proof

let x, y, z be Element of X; :: thesis: ((x \ y) \ z) \ ((x \ z) \ y) = 0. X
(((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z)))) \ ((x \ (x \ z)) \ z) = 0. X by A6;
then (((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z)))) \ (0. X) = 0. X by A6;
then A15: ((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z))) = 0. X by A7;
((x \ y) \ (x \ (x \ z))) \ ((x \ z) \ y) = 0. X by A6;
hence ((x \ y) \ z) \ ((x \ z) \ y) = 0. X by A11, A15; :: thesis: verum

end;

A16: for x, y, z being Element of X st x \ y = 0. X holds
( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X )

proof

let x, y, z be Element of X; :: thesis: ( x \ y = 0. X implies ( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X ) )
assume A17: x \ y = 0. X ; :: thesis: ( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X )
( ((z \ y) \ (z \ x)) \ (x \ y) = 0. X & ((x \ z) \ (x \ y)) \ (y \ z) = 0. X ) by A6;
hence ( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X ) by A9, A17; :: thesis: verum

end;

for x, y, z being Element of X holds ((x \ y) \ (z \ y)) \ (x \ z) = 0. X

proof

let x, y, z be Element of X; :: thesis: ((x \ y) \ (z \ y)) \ (x \ z) = 0. X
((x \ y) \ (x \ z)) \ (z \ y) = 0. X by A6;
then ((x \ y) \ (z \ y)) \ ((x \ y) \ ((x \ y) \ (x \ z))) = 0. X by A16;
then (((x \ y) \ (z \ y)) \ (x \ z)) \ (((x \ y) \ ((x \ y) \ (x \ z))) \ (x \ z)) = 0. X by A16;
then (((x \ y) \ (z \ y)) \ (x \ z)) \ (0. X) = 0. X by A6;
hence ((x \ y) \ (z \ y)) \ (x \ z) = 0. X by A7; :: thesis: verum

end;

hence X is BCI-algebra by A4, A5, A14, Def3, Def4; :: thesis: verum