let X be non empty BCIStr_0 ; :: thesis: ( X is BCK-implicative BCK-algebra iff for x, y, z being Element of X holds

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

thus ( X is BCK-implicative BCK-algebra implies for x, y, z being Element of X holds

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

( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) ) ) implies X is BCK-implicative BCK-algebra )

( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) ) ; :: thesis: X is BCK-implicative BCK-algebra

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

x = y

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

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

thus ( X is BCK-implicative BCK-algebra implies for x, y, z being Element of X holds

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

( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) ) ) implies X is BCK-implicative BCK-algebra )

proof

assume A4:
for x, y, z being Element of X holds
assume A1:
X is BCK-implicative BCK-algebra
; :: thesis: for x, y, z being Element of X holds

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

then A2: X is commutative BCK-algebra by Th34;

let x, y, z be Element of X; :: thesis: ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) )

A3: x \ ((0. X) \ y) = x \ (y `)

.= x \ (0. X) by A1, BCIALG_1:def 8

.= x by A1, BCIALG_1:2 ;

((y \ z) \ (y \ x)) \ (x \ y) = ((y \ z) \ (x \ y)) \ (y \ x) by A1, BCIALG_1:7

.= ((y \ (x \ y)) \ z) \ (y \ x) by A1, BCIALG_1:7

.= (y \ z) \ (y \ x) by A1, Def12

.= (y \ (y \ x)) \ z by A1, BCIALG_1:7

.= (x \ (x \ y)) \ z by A2, Def1

.= (x \ z) \ (x \ y) by A1, BCIALG_1:7 ;

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

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

then A2: X is commutative BCK-algebra by Th34;

let x, y, z be Element of X; :: thesis: ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) )

A3: x \ ((0. X) \ y) = x \ (y `)

.= x \ (0. X) by A1, BCIALG_1:def 8

.= x by A1, BCIALG_1:2 ;

((y \ z) \ (y \ x)) \ (x \ y) = ((y \ z) \ (x \ y)) \ (y \ x) by A1, BCIALG_1:7

.= ((y \ (x \ y)) \ z) \ (y \ x) by A1, BCIALG_1:7

.= (y \ z) \ (y \ x) by A1, Def12

.= (y \ (y \ x)) \ z by A1, BCIALG_1:7

.= (x \ (x \ y)) \ z by A2, Def1

.= (x \ z) \ (x \ y) by A1, BCIALG_1:7 ;

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

( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) ) ; :: thesis: X is BCK-implicative BCK-algebra

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

proof

A6:
for x, y being Element of X st x \ y = 0. X & y \ x = 0. X holds
let x, y be Element of X; :: thesis: x \ (0. X) = x

(0. X) \ ((0. X) \ (0. X)) = 0. X by A4;

hence x \ (0. X) = x by A4; :: thesis: verum

end;(0. X) \ ((0. X) \ (0. X)) = 0. X by A4;

hence x \ (0. X) = x by A4; :: thesis: verum

x = y

proof

A7:
for x, y being Element of X holds x \ (x \ y) = (y \ (y \ x)) \ (x \ y)
let x, y be Element of X; :: thesis: ( x \ y = 0. X & y \ x = 0. X implies x = y )

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

then (x \ (0. X)) \ (0. X) = ((y \ (0. X)) \ (0. X)) \ (0. X) by A4

.= (y \ (0. X)) \ (0. X) by A5 ;

then x \ (0. X) = (y \ (0. X)) \ (0. X) by A5

.= y \ (0. X) by A5 ;

hence x = y \ (0. X) by A5

.= y by A5 ;

:: thesis: verum

end;assume ( x \ y = 0. X & y \ x = 0. X ) ; :: thesis: x = y

then (x \ (0. X)) \ (0. X) = ((y \ (0. X)) \ (0. X)) \ (0. X) by A4

.= (y \ (0. X)) \ (0. X) by A5 ;

then x \ (0. X) = (y \ (0. X)) \ (0. X) by A5

.= y \ (0. X) by A5 ;

hence x = y \ (0. X) by A5

.= y by A5 ;

:: thesis: verum

proof

A8:
for y being Element of X holds y \ y = 0. X
let x, y be Element of X; :: thesis: x \ (x \ y) = (y \ (y \ x)) \ (x \ y)

x \ (x \ y) = (x \ (0. X)) \ (x \ y) by A5

.= ((y \ (0. X)) \ (y \ x)) \ (x \ y) by A4 ;

hence x \ (x \ y) = (y \ (y \ x)) \ (x \ y) by A5; :: thesis: verum

end;x \ (x \ y) = (x \ (0. X)) \ (x \ y) by A5

.= ((y \ (0. X)) \ (y \ x)) \ (x \ y) by A4 ;

hence x \ (x \ y) = (y \ (y \ x)) \ (x \ y) by A5; :: thesis: verum

proof

A9:
for x being Element of X holds (0. X) \ x = 0. X
let y be Element of X; :: thesis: y \ y = 0. X

(0. X) \ ((0. X) \ y) = (y \ (y \ (0. X))) \ ((0. X) \ y) by A7

.= (y \ y) \ ((0. X) \ y) by A5

.= y \ y by A4 ;

hence y \ y = 0. X by A4; :: thesis: verum

end;(0. X) \ ((0. X) \ y) = (y \ (y \ (0. X))) \ ((0. X) \ y) by A7

.= (y \ y) \ ((0. X) \ y) by A5

.= y \ y by A4 ;

hence y \ y = 0. X by A4; :: thesis: verum

proof

A10:
for x, y being Element of X holds (x \ y) \ x = 0. X
let x be Element of X; :: thesis: (0. X) \ x = 0. X

((0. X) \ x) \ ((0. X) \ x) = (0. X) \ x by A4;

hence (0. X) \ x = 0. X by A8; :: thesis: verum

end;((0. X) \ x) \ ((0. X) \ x) = (0. X) \ x by A4;

hence (0. X) \ x = 0. X by A8; :: thesis: verum

proof

A11:
for x, y, z being Element of X holds ((x \ z) \ (x \ y)) \ ((y \ z) \ (y \ x)) = 0. X
let x, y be Element of X; :: thesis: (x \ y) \ x = 0. X

(x \ y) \ x = (x \ y) \ (x \ (0. X)) by A5

.= (((0. X) \ y) \ ((0. X) \ x)) \ (x \ (0. X)) by A4

.= ((0. X) \ ((0. X) \ x)) \ (x \ (0. X)) by A9

.= (0. X) \ (x \ (0. X)) by A9 ;

hence (x \ y) \ x = 0. X by A9; :: thesis: verum

end;(x \ y) \ x = (x \ y) \ (x \ (0. X)) by A5

.= (((0. X) \ y) \ ((0. X) \ x)) \ (x \ (0. X)) by A4

.= ((0. X) \ ((0. X) \ x)) \ (x \ (0. X)) by A9

.= (0. X) \ (x \ (0. X)) by A9 ;

hence (x \ y) \ x = 0. X by A9; :: thesis: verum

proof

A12:
for x, y, z being Element of X holds (x \ z) \ (x \ y) = (y \ z) \ (y \ x)
let x, y, z be Element of X; :: thesis: ((x \ z) \ (x \ y)) \ ((y \ z) \ (y \ x)) = 0. X

(((y \ z) \ (y \ x)) \ (x \ y)) \ ((y \ z) \ (y \ x)) = 0. X by A10;

hence ((x \ z) \ (x \ y)) \ ((y \ z) \ (y \ x)) = 0. X by A4; :: thesis: verum

end;(((y \ z) \ (y \ x)) \ (x \ y)) \ ((y \ z) \ (y \ x)) = 0. X by A10;

hence ((x \ z) \ (x \ y)) \ ((y \ z) \ (y \ x)) = 0. X by A4; :: thesis: verum

proof

then A13:
X is commutative BCK-algebra
by A4, Th6;
let x, y, z be Element of X; :: thesis: (x \ z) \ (x \ y) = (y \ z) \ (y \ x)

( ((y \ z) \ (y \ x)) \ ((x \ z) \ (x \ y)) = 0. X & ((x \ z) \ (x \ y)) \ ((y \ z) \ (y \ x)) = 0. X ) by A11;

hence (x \ z) \ (x \ y) = (y \ z) \ (y \ x) by A6; :: thesis: verum

end;( ((y \ z) \ (y \ x)) \ ((x \ z) \ (x \ y)) = 0. X & ((x \ z) \ (x \ y)) \ ((y \ z) \ (y \ x)) = 0. X ) by A11;

hence (x \ z) \ (x \ y) = (y \ z) \ (y \ x) by A6; :: thesis: verum

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

proof

hence
X is BCK-implicative BCK-algebra
by A4, A12, Th6, Th35; :: thesis: verum
let x, y be Element of X; :: thesis: (x \ (x \ y)) \ (x \ y) = y \ (y \ x)

x \ (x \ y) = y \ (y \ x) by A13, Def1;

hence (x \ (x \ y)) \ (x \ y) = y \ (y \ x) by A7; :: thesis: verum

end;x \ (x \ y) = y \ (y \ x) by A13, Def1;

hence (x \ (x \ y)) \ (x \ y) = y \ (y \ x) by A7; :: thesis: verum