let X be non empty BCIStr_0 ; :: thesis:
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:

let x, y, z be Element of X; :: thesis:
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

let x, y, z be Element of X; :: thesis:
( ((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:

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:

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:

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:
A7: for x being Element of X st x \ (0. X) = 0. X holds
x = 0. X

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

end;

let x be Element of X; :: thesis:
(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:

end;

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

let x, y, z be Element of X; :: thesis:
assume that
A12: x \ y = 0. X and
A13: y \ z = 0. X ; :: thesis:
((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:

end;

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

let x, y, z be Element of X; :: thesis:
(((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:

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 )

let x, y, z be Element of X; :: thesis:
assume A17: x \ y = 0. X ; :: thesis:
( ((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:

end;

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

let x, y, z be Element of X; :: thesis:
((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:

end;