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

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 ) ) ) by A1; :: thesis: verum

end;

assume A4: ( 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 BCI-algebra
A5: 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 A6: x \ (0. X) = 0. X ; :: thesis: x = 0. X
then x ` = (x \ (x \ x)) \ x by A4, Def5
.= 0. X by A4 ;
hence x = 0. X by A4, A6, Def7; :: thesis: verum

end;

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

proof

let x be Element of X; :: thesis: x \ (0. X) = x
A8: 0. X = (x \ (x \ x)) \ x by A4
.= (x \ (0. X)) \ x by A4, Def5 ;
(x \ (x \ (0. X))) \ (0. X) = 0. X by A4;
then x \ (x \ (0. X)) = 0. X by A5;
hence x \ (0. X) = x by A4, A8, Def7; :: thesis: verum

end;

A9: 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 A10: ( x \ y = 0. X & y \ z = 0. X ) ; :: thesis: x \ z = 0. X
((x \ z) \ (x \ y)) \ (y \ z) = 0. X by A4;
then (x \ z) \ (x \ y) = 0. X by A7, A10;
hence x \ z = 0. X by A7, A10; :: thesis: verum

end;

A11: 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 A12: x \ y = 0. X ; :: thesis: ( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X )
A13: ((z \ y) \ (z \ x)) \ (x \ y) = 0. X by A4;
((x \ z) \ (x \ y)) \ (y \ z) = 0. X by A4;
hence ( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X ) by A7, A12, A13; :: thesis: verum

end;

A14: 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 A4;
then ((x \ y) \ (z \ y)) \ ((x \ y) \ ((x \ y) \ (x \ z))) = 0. X by A11;
then (((x \ y) \ (z \ y)) \ (x \ z)) \ (((x \ y) \ ((x \ y) \ (x \ z))) \ (x \ z)) = 0. X by A11;
then (((x \ y) \ (z \ y)) \ (x \ z)) \ (0. X) = 0. X by A4;
hence ((x \ y) \ (z \ y)) \ (x \ z) = 0. X by A5; :: thesis: verum

end;

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 A4;
then (((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z)))) \ (0. X) = 0. X by A4;
then A15: ((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z))) = 0. X by A5;
((x \ y) \ (x \ (x \ z))) \ ((x \ z) \ y) = 0. X by A4;
hence ((x \ y) \ z) \ ((x \ z) \ y) = 0. X by A9, A15; :: thesis: verum

end;

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