let X be non empty BCIStr_1 ; :: thesis: ( X is commutative BCK-Algebra_with_Condition(S) 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) \ z = x \ (y * z) ) )

thus ( X is commutative BCK-Algebra_with_Condition(S) 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) \ z = x \ (y * z) ) ) :: 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) \ z = x \ (y * z) ) ) implies X is commutative BCK-Algebra_with_Condition(S) )

( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) & (x \ y) \ z = x \ (y * z) ) ) implies X is commutative BCK-Algebra_with_Condition(S) ) :: thesis: verum

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

thus ( X is commutative BCK-Algebra_with_Condition(S) 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) \ z = x \ (y * z) ) ) :: 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) \ z = x \ (y * z) ) ) implies X is commutative BCK-Algebra_with_Condition(S) )

proof

thus
( ( for x, y, z being Element of X holds
assume A1:
X is commutative BCK-Algebra_with_Condition(S)
; :: 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) \ z = x \ (y * z) )

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

(x \ (x \ y)) \ z = (y \ (y \ x)) \ z by A1, Def9;

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

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

(0. X) \ y = y `

.= 0. X by A1, BCIALG_1:def 8 ;

hence ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) & (x \ y) \ z = x \ (y * z) ) by A1, A2, Th11, BCIALG_1:2; :: thesis: verum

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

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

(x \ (x \ y)) \ z = (y \ (y \ x)) \ z by A1, Def9;

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

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

(0. X) \ y = y `

.= 0. X by A1, BCIALG_1:def 8 ;

hence ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) & (x \ y) \ z = x \ (y * z) ) by A1, A2, Th11, BCIALG_1:2; :: thesis: verum

( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) & (x \ y) \ z = x \ (y * z) ) ) implies X is commutative BCK-Algebra_with_Condition(S) ) :: thesis: verum

proof

assume A3:
for x, y, z being Element of X holds

( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) & (x \ y) \ z = x \ (y * z) ) ; :: thesis: X is commutative BCK-Algebra_with_Condition(S)

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

x = y

x \ z = 0. X

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

hence X is commutative BCK-Algebra_with_Condition(S) by A3, A6, A5, A14, A12, A17, Def2, Def9, BCIALG_1:def 3, BCIALG_1:def 4, BCIALG_1:def 5, BCIALG_1:def 7, BCIALG_1:def 8; :: thesis: verum

end;( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) & (x \ y) \ z = x \ (y * z) ) ; :: thesis: X is commutative BCK-Algebra_with_Condition(S)

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

proof

A5:
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 A3;

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

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

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

x = y

proof

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

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

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

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

.= y by A4 ;

:: 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) by A3;

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

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

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

.= y by A4 ;

:: thesis: verum

proof

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

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

then x \ x = ((0. X) \ (0. X)) \ ((0. X) \ x) by A3

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

.= 0. X by A3 ;

hence x \ x = 0. X ; :: thesis: verum

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

then x \ x = ((0. X) \ (0. X)) \ ((0. X) \ x) by A3

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

.= 0. X by A3 ;

hence x \ x = 0. X ; :: thesis: verum

proof

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

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

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

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

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

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

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

proof

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

((x \ y) \ (x \ z)) \ (z \ y) = ((z \ y) \ (z \ x)) \ (z \ y) by A3

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

.= ((0. X) \ (z \ x)) \ ((0. X) \ (z \ y)) by A3

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

.= 0. X by A7 ;

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

end;((x \ y) \ (x \ z)) \ (z \ y) = ((z \ y) \ (z \ x)) \ (z \ y) by A3

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

.= ((0. X) \ (z \ x)) \ ((0. X) \ (z \ y)) by A3

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

.= 0. X by A7 ;

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

x \ z = 0. X

proof

A12:
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

A10: x \ y = 0. X and

A11: y \ z = 0. X ; :: thesis: x \ z = 0. X

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

then (x \ z) \ (x \ y) = 0. X by A4, A11;

hence x \ z = 0. X by A4, A10; :: thesis: verum

end;assume that

A10: x \ y = 0. X and

A11: y \ z = 0. X ; :: thesis: x \ z = 0. X

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

then (x \ z) \ (x \ y) = 0. X by A4, A11;

hence x \ z = 0. X by A4, A10; :: thesis: verum

proof

A14:
for x, y being Element of X holds x \ (x \ y) = y \ (y \ x)
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 A8;

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

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

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

then A13: ((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z))) = 0. X by A4;

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

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

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

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

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

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

then A13: ((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z))) = 0. X by A4;

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

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

proof

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

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

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

.= y \ (y \ x) by A3 ;

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

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

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

.= y \ (y \ x) by A3 ;

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

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

proof

A17:
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 A16: 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 A8;

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

end;assume A16: 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 A8;

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

proof

for x being Element of X holds x ` = 0. X
by A7;
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 A8;

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

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

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

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

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

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

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

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

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

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

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

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

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

hence X is commutative BCK-Algebra_with_Condition(S) by A3, A6, A5, A14, A12, A17, Def2, Def9, BCIALG_1:def 3, BCIALG_1:def 4, BCIALG_1:def 5, BCIALG_1:def 7, BCIALG_1:def 8; :: thesis: verum