let X be non empty BCIStr_1 ; ( 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) ) )
( ( 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
assume A1:
X is
commutative BCK-Algebra_with_Condition(S)
;
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;
( 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;
verum
end;
thus
( ( 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) )
verumproof
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) )
;
X is commutative BCK-Algebra_with_Condition(S)
A4:
for
x,
y being
Element of
X holds
x \ (0. X) = x
A5:
for
x,
y being
Element of
X st
x \ y = 0. X &
y \ x = 0. X holds
x = y
A6:
for
x being
Element of
X holds
x \ x = 0. X
A7:
for
x being
Element of
X holds
(0. X) \ x = 0. X
A8:
for
x,
y,
z being
Element of
X holds
((x \ y) \ (x \ z)) \ (z \ y) = 0. X
A9:
for
x,
y,
z being
Element of
X st
x \ y = 0. X &
y \ z = 0. X holds
x \ z = 0. X
A12:
for
x,
y,
z being
Element of
X holds
((x \ y) \ z) \ ((x \ z) \ y) = 0. X
A14:
for
x,
y being
Element of
X holds
x \ (x \ y) = y \ (y \ x)
A15:
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 )
A17:
for
x,
y,
z being
Element of
X holds
((x \ y) \ (z \ y)) \ (x \ z) = 0. X
for
x being
Element of
X holds
x ` = 0. X
by A7;
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;
verum
end;