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 )

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

x \ z = 0. X

( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X )

( ((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 that
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 ) ) )

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ) ) ; :: thesis: verum

end;( ((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 ) )

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 & 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

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;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

then
(x \ (x \ y)) \ y = (x \ y) \ (x \ y)
;
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;( ((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

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

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ) ) ; :: thesis: verum

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

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

proof

A11:
for x, y, z being Element of X st x \ y = 0. X & y \ z = 0. X holds
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;(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

x \ z = 0. X

proof

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 = 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;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

proof

A16:
for x, y, z being Element of X st x \ y = 0. X holds
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;(((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

( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X )

proof

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 = 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;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

proof

hence
X is BCI-algebra
by A4, A5, A14, Def3, Def4; :: thesis: verum
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;((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