let X be non empty BCIStr_0 ; ( 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 ) ) ) )
( 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 )
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 )
; X is BCI-algebra
A7:
for x being Element of X st x \ (0. X) = 0. X holds
x = 0. X
A9:
for x being Element of X holds x \ (0. X) = x
A11:
for x, y, z being Element of X st x \ y = 0. X & y \ z = 0. X holds
x \ z = 0. X
A14:
for x, y, z being Element of X holds ((x \ y) \ z) \ ((x \ z) \ y) = 0. X
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 )
for x, y, z being Element of X holds ((x \ y) \ (z \ y)) \ (x \ z) = 0. X
hence
X is BCI-algebra
by A4, A5, A14, Def3, Def4; verum