:: Several Classes of {BCK}-algebras and Their Properties
:: by Tao Sun , Dahai Hu and Xiquan Liang
::
:: Received September 19, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users
begin
definition
let
IT
be non
empty
BCIStr_0
;
attr
IT
is
commutative
means
:
Def1
:
:: BCIALG_3:def 1
for
x
,
y
being
Element
of
IT
holds
x
\
(
x
\
y
)
=
y
\
(
y
\
x
)
;
end;
::
deftheorem
Def1
defines
commutative
BCIALG_3:def 1 :
for
IT
being non
empty
BCIStr_0
holds
(
IT
is
commutative
iff for
x
,
y
being
Element
of
IT
holds
x
\
(
x
\
y
)
=
y
\
(
y
\
x
)
);
registration
cluster
BCI-EXAMPLE
->
commutative
;
coherence
BCI-EXAMPLE
is
commutative
proof
end;
end;
registration
cluster
non
empty
being_B
being_C
being_I
being_BCI-4
being_BCK-5
commutative
for
BCIStr_0
;
existence
ex
b
1
being
BCK-algebra
st
b
1
is
commutative
proof
end;
end;
theorem
Th1
:
:: BCIALG_3:1
for
X
being
BCK-algebra
holds
(
X
is
commutative
BCK-algebra
iff for
x
,
y
being
Element
of
X
holds
x
\
(
x
\
y
)
<=
y
\
(
y
\
x
)
)
proof
end;
theorem
Th2
:
:: BCIALG_3:2
for
X
being
BCK-algebra
for
x
,
y
being
Element
of
X
holds
(
x
\
(
x
\
y
)
<=
y
&
x
\
(
x
\
y
)
<=
x
)
proof
end;
theorem
Th3
:
:: BCIALG_3:3
for
X
being
BCK-algebra
holds
(
X
is
commutative
BCK-algebra
iff for
x
,
y
being
Element
of
X
holds
x
\
y
=
x
\
(
y
\
(
y
\
x
)
)
)
proof
end;
theorem
Th4
:
:: BCIALG_3:4
for
X
being
BCK-algebra
holds
(
X
is
commutative
BCK-algebra
iff for
x
,
y
being
Element
of
X
holds
x
\
(
x
\
y
)
=
y
\
(
y
\
(
x
\
(
x
\
y
)
)
)
)
proof
end;
theorem
Th5
:
:: BCIALG_3:5
for
X
being
BCK-algebra
holds
(
X
is
commutative
BCK-algebra
iff for
x
,
y
being
Element
of
X
st
x
<=
y
holds
x
=
y
\
(
y
\
x
)
)
proof
end;
theorem
Th6
:
:: BCIALG_3:6
for
X
being non
empty
BCIStr_0
holds
(
X
is
commutative
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
)
) )
proof
end;
theorem
:: BCIALG_3:7
for
X
being
BCK-algebra
st
X
is
commutative
BCK-algebra
holds
for
x
,
y
being
Element
of
X
st
x
\
y
=
x
holds
y
\
x
=
y
proof
end;
theorem
Th8
:
:: BCIALG_3:8
for
X
being
BCK-algebra
st
X
is
commutative
BCK-algebra
holds
for
x
,
y
,
a
being
Element
of
X
st
y
<=
a
holds
(
a
\
x
)
\
(
a
\
y
)
=
y
\
x
proof
end;
theorem
:: BCIALG_3:9
for
X
being
BCK-algebra
st
X
is
commutative
BCK-algebra
holds
for
x
,
y
being
Element
of
X
holds
(
x
\
y
=
x
iff
y
\
(
y
\
x
)
=
0.
X
)
proof
end;
theorem
:: BCIALG_3:10
for
X
being
BCK-algebra
st
X
is
commutative
BCK-algebra
holds
for
x
,
y
being
Element
of
X
holds
(
x
\
(
y
\
(
y
\
x
)
)
=
x
\
y
&
(
x
\
y
)
\
(
(
x
\
y
)
\
x
)
=
x
\
y
)
proof
end;
theorem
:: BCIALG_3:11
for
X
being
BCK-algebra
st
X
is
commutative
BCK-algebra
holds
for
x
,
y
,
a
being
Element
of
X
st
x
<=
a
holds
(
a
\
y
)
\
(
(
a
\
y
)
\
(
a
\
x
)
)
=
(
a
\
y
)
\
(
x
\
y
)
by
Th8
;
definition
let
X
be
BCI-algebra
;
let
a
be
Element
of
X
;
attr
a
is
being_greatest
means
:
Def2
:
:: BCIALG_3:def 2
for
x
being
Element
of
X
holds
x
\
a
=
0.
X
;
attr
a
is
being_positive
means
:: BCIALG_3:def 3
(
0.
X
)
\
a
=
0.
X
;
end;
::
deftheorem
Def2
defines
being_greatest
BCIALG_3:def 2 :
for
X
being
BCI-algebra
for
a
being
Element
of
X
holds
(
a
is
being_greatest
iff for
x
being
Element
of
X
holds
x
\
a
=
0.
X
);
::
deftheorem
defines
being_positive
BCIALG_3:def 3 :
for
X
being
BCI-algebra
for
a
being
Element
of
X
holds
(
a
is
being_positive
iff
(
0.
X
)
\
a
=
0.
X
);
begin
definition
let
IT
be
BCI-algebra
;
attr
IT
is
BCI-commutative
means
:
Def4
:
:: BCIALG_3:def 4
for
x
,
y
being
Element
of
IT
st
x
\
y
=
0.
IT
holds
x
=
y
\
(
y
\
x
)
;
attr
IT
is
BCI-weakly-commutative
means
:
Def5
:
:: BCIALG_3:def 5
for
x
,
y
being
Element
of
IT
holds
(
x
\
(
x
\
y
)
)
\
(
(
0.
IT
)
\
(
x
\
y
)
)
=
y
\
(
y
\
x
)
;
end;
::
deftheorem
Def4
defines
BCI-commutative
BCIALG_3:def 4 :
for
IT
being
BCI-algebra
holds
(
IT
is
BCI-commutative
iff for
x
,
y
being
Element
of
IT
st
x
\
y
=
0.
IT
holds
x
=
y
\
(
y
\
x
)
);
::
deftheorem
Def5
defines
BCI-weakly-commutative
BCIALG_3:def 5 :
for
IT
being
BCI-algebra
holds
(
IT
is
BCI-weakly-commutative
iff for
x
,
y
being
Element
of
IT
holds
(
x
\
(
x
\
y
)
)
\
(
(
0.
IT
)
\
(
x
\
y
)
)
=
y
\
(
y
\
x
)
);
registration
cluster
BCI-EXAMPLE
->
BCI-commutative
BCI-weakly-commutative
;
coherence
(
BCI-EXAMPLE
is
BCI-commutative
&
BCI-EXAMPLE
is
BCI-weakly-commutative
)
proof
end;
end;
registration
cluster
non
empty
being_B
being_C
being_I
being_BCI-4
BCI-commutative
BCI-weakly-commutative
for
BCIStr_0
;
existence
ex
b
1
being
BCI-algebra
st
(
b
1
is
BCI-commutative
&
b
1
is
BCI-weakly-commutative
)
proof
end;
end;
theorem
:: BCIALG_3:12
for
X
being
BCI-algebra
st ex
a
being
Element
of
X
st
a
is
being_greatest
holds
X
is
BCK-algebra
proof
end;
theorem
:: BCIALG_3:13
for
X
being
BCI-algebra
st
X
is
p-Semisimple
holds
(
X
is
BCI-commutative
&
X
is
BCI-weakly-commutative
)
proof
end;
theorem
:: BCIALG_3:14
for
X
being
commutative
BCK-algebra
holds
(
X
is
BCI-commutative
BCI-algebra
&
X
is
BCI-weakly-commutative
BCI-algebra
)
proof
end;
theorem
:: BCIALG_3:15
for
X
being
BCK-algebra
st
X
is
BCI-weakly-commutative
BCI-algebra
holds
X
is
BCI-commutative
proof
end;
theorem
Th16
:
:: BCIALG_3:16
for
X
being
BCI-algebra
holds
(
X
is
BCI-commutative
iff for
x
,
y
being
Element
of
X
holds
x
\
(
x
\
y
)
=
y
\
(
y
\
(
x
\
(
x
\
y
)
)
)
)
proof
end;
theorem
Th17
:
:: BCIALG_3:17
for
X
being
BCI-algebra
holds
(
X
is
BCI-commutative
iff for
x
,
y
being
Element
of
X
holds
(
x
\
(
x
\
y
)
)
\
(
y
\
(
y
\
x
)
)
=
(
0.
X
)
\
(
x
\
y
)
)
proof
end;
theorem
:: BCIALG_3:18
for
X
being
BCI-algebra
holds
(
X
is
BCI-commutative
iff for
a
being
Element
of
AtomSet
X
for
x
,
y
being
Element
of
BranchV
a
holds
x
\
(
x
\
y
)
=
y
\
(
y
\
x
)
)
proof
end;
theorem
:: BCIALG_3:19
for
X
being non
empty
BCIStr_0
holds
(
X
is
BCI-commutative
BCI-algebra
iff for
x
,
y
,
z
being
Element
of
X
holds
(
(
(
x
\
y
)
\
(
x
\
z
)
)
\
(
z
\
y
)
=
0.
X
&
x
\
(
0.
X
)
=
x
&
x
\
(
x
\
y
)
=
y
\
(
y
\
(
x
\
(
x
\
y
)
)
)
) )
proof
end;
theorem
:: BCIALG_3:20
for
X
being
BCI-algebra
holds
(
X
is
BCI-commutative
iff for
x
,
y
,
z
being
Element
of
X
st
x
<=
z
&
z
\
y
<=
z
\
x
holds
x
<=
y
)
proof
end;
theorem
:: BCIALG_3:21
for
X
being
BCI-algebra
holds
(
X
is
BCI-commutative
iff for
x
,
y
,
z
being
Element
of
X
st
x
<=
y
&
x
<=
z
holds
x
<=
y
\
(
y
\
z
)
)
proof
end;
begin
definition
let
IT
be
BCK-algebra
;
attr
IT
is
bounded
means
:: BCIALG_3:def 6
ex
a
being
Element
of
IT
st
a
is
being_greatest
;
end;
::
deftheorem
defines
bounded
BCIALG_3:def 6 :
for
IT
being
BCK-algebra
holds
(
IT
is
bounded
iff ex
a
being
Element
of
IT
st
a
is
being_greatest
);
registration
cluster
BCI-EXAMPLE
->
bounded
;
coherence
BCI-EXAMPLE
is
bounded
proof
end;
end;
registration
cluster
non
empty
being_B
being_C
being_I
being_BCI-4
being_BCK-5
commutative
bounded
for
BCIStr_0
;
existence
ex
b
1
being
BCK-algebra
st
(
b
1
is
bounded
&
b
1
is
commutative
)
proof
end;
end;
definition
let
IT
be
bounded
BCK-algebra
;
attr
IT
is
involutory
means
:
Def7
:
:: BCIALG_3:def 7
for
a
being
Element
of
IT
st
a
is
being_greatest
holds
for
x
being
Element
of
IT
holds
a
\
(
a
\
x
)
=
x
;
end;
::
deftheorem
Def7
defines
involutory
BCIALG_3:def 7 :
for
IT
being
bounded
BCK-algebra
holds
(
IT
is
involutory
iff for
a
being
Element
of
IT
st
a
is
being_greatest
holds
for
x
being
Element
of
IT
holds
a
\
(
a
\
x
)
=
x
);
theorem
Th22
:
:: BCIALG_3:22
for
X
being
bounded
BCK-algebra
holds
(
X
is
involutory
iff for
a
being
Element
of
X
st
a
is
being_greatest
holds
for
x
,
y
being
Element
of
X
holds
x
\
y
=
(
a
\
y
)
\
(
a
\
x
)
)
proof
end;
theorem
Th23
:
:: BCIALG_3:23
for
X
being
bounded
BCK-algebra
holds
(
X
is
involutory
iff for
a
being
Element
of
X
st
a
is
being_greatest
holds
for
x
,
y
being
Element
of
X
holds
x
\
(
a
\
y
)
=
y
\
(
a
\
x
)
)
proof
end;
theorem
:: BCIALG_3:24
for
X
being
bounded
BCK-algebra
holds
(
X
is
involutory
iff for
a
being
Element
of
X
st
a
is
being_greatest
holds
for
x
,
y
being
Element
of
X
st
x
<=
a
\
y
holds
y
<=
a
\
x
)
proof
end;
definition
let
IT
be
BCK-algebra
;
let
a
be
Element
of
IT
;
attr
a
is
being_Iseki
means
:
Def8
:
:: BCIALG_3:def 8
for
x
being
Element
of
IT
holds
(
x
\
a
=
0.
IT
&
a
\
x
=
a
);
end;
::
deftheorem
Def8
defines
being_Iseki
BCIALG_3:def 8 :
for
IT
being
BCK-algebra
for
a
being
Element
of
IT
holds
(
a
is
being_Iseki
iff for
x
being
Element
of
IT
holds
(
x
\
a
=
0.
IT
&
a
\
x
=
a
) );
definition
let
IT
be
BCK-algebra
;
attr
IT
is
Iseki_extension
means
:: BCIALG_3:def 9
ex
a
being
Element
of
IT
st
a
is
being_Iseki
;
end;
::
deftheorem
defines
Iseki_extension
BCIALG_3:def 9 :
for
IT
being
BCK-algebra
holds
(
IT
is
Iseki_extension
iff ex
a
being
Element
of
IT
st
a
is
being_Iseki
);
registration
cluster
BCI-EXAMPLE
->
Iseki_extension
;
coherence
BCI-EXAMPLE
is
Iseki_extension
proof
end;
end;
:: Commutative Ideal
definition
let
X
be
BCK-algebra
;
mode
Commutative-Ideal
of
X
->
non
empty
Subset
of
X
means
:
Def10
:
:: BCIALG_3:def 10
(
0.
X
in
it
& ( for
x
,
y
,
z
being
Element
of
X
st
(
x
\
y
)
\
z
in
it
&
z
in
it
holds
x
\
(
y
\
(
y
\
x
)
)
in
it
) );
existence
ex
b
1
being non
empty
Subset
of
X
st
(
0.
X
in
b
1
& ( for
x
,
y
,
z
being
Element
of
X
st
(
x
\
y
)
\
z
in
b
1
&
z
in
b
1
holds
x
\
(
y
\
(
y
\
x
)
)
in
b
1
) )
proof
end;
end;
::
deftheorem
Def10
defines
Commutative-Ideal
BCIALG_3:def 10 :
for
X
being
BCK-algebra
for
b
2
being non
empty
Subset
of
X
holds
(
b
2
is
Commutative-Ideal
of
X
iff (
0.
X
in
b
2
& ( for
x
,
y
,
z
being
Element
of
X
st
(
x
\
y
)
\
z
in
b
2
&
z
in
b
2
holds
x
\
(
y
\
(
y
\
x
)
)
in
b
2
) ) );
theorem
:: BCIALG_3:25
for
X
being
BCK-algebra
for
IT
being non
empty
Subset
of
X
st
IT
is
Commutative-Ideal
of
X
holds
for
x
,
y
being
Element
of
X
st
x
\
y
in
IT
holds
x
\
(
y
\
(
y
\
x
)
)
in
IT
proof
end;
theorem
Th26
:
:: BCIALG_3:26
for
X
being
BCK-algebra
for
IT
being non
empty
Subset
of
X
for
X
being
BCK-algebra
st
IT
is
Commutative-Ideal
of
X
holds
IT
is
Ideal
of
X
proof
end;
theorem
:: BCIALG_3:27
for
X
being
BCK-algebra
for
IT
being non
empty
Subset
of
X
st
IT
is
Commutative-Ideal
of
X
holds
for
x
,
y
being
Element
of
X
st
x
\
(
x
\
y
)
in
IT
holds
(
y
\
(
y
\
x
)
)
\
(
x
\
y
)
in
IT
proof
end;
begin
definition
let
IT
be
BCK-algebra
;
attr
IT
is
BCK-positive-implicative
means
:
Def11
:
:: BCIALG_3:def 11
for
x
,
y
,
z
being
Element
of
IT
holds
(
x
\
y
)
\
z
=
(
x
\
z
)
\
(
y
\
z
)
;
attr
IT
is
BCK-implicative
means
:
Def12
:
:: BCIALG_3:def 12
for
x
,
y
being
Element
of
IT
holds
x
\
(
y
\
x
)
=
x
;
end;
::
deftheorem
Def11
defines
BCK-positive-implicative
BCIALG_3:def 11 :
for
IT
being
BCK-algebra
holds
(
IT
is
BCK-positive-implicative
iff for
x
,
y
,
z
being
Element
of
IT
holds
(
x
\
y
)
\
z
=
(
x
\
z
)
\
(
y
\
z
)
);
::
deftheorem
Def12
defines
BCK-implicative
BCIALG_3:def 12 :
for
IT
being
BCK-algebra
holds
(
IT
is
BCK-implicative
iff for
x
,
y
being
Element
of
IT
holds
x
\
(
y
\
x
)
=
x
);
registration
cluster
BCI-EXAMPLE
->
BCK-positive-implicative
BCK-implicative
;
coherence
(
BCI-EXAMPLE
is
BCK-positive-implicative
&
BCI-EXAMPLE
is
BCK-implicative
)
proof
end;
end;
registration
cluster
non
empty
being_B
being_C
being_I
being_BCI-4
being_BCK-5
commutative
bounded
Iseki_extension
BCK-positive-implicative
BCK-implicative
for
BCIStr_0
;
existence
ex
b
1
being
BCK-algebra
st
(
b
1
is
Iseki_extension
&
b
1
is
BCK-positive-implicative
&
b
1
is
BCK-implicative
&
b
1
is
bounded
&
b
1
is
commutative
)
proof
end;
end;
theorem
Th28
:
:: BCIALG_3:28
for
X
being
BCK-algebra
holds
(
X
is
BCK-positive-implicative
BCK-algebra
iff for
x
,
y
being
Element
of
X
holds
x
\
y
=
(
x
\
y
)
\
y
)
proof
end;
theorem
Th29
:
:: BCIALG_3:29
for
X
being
BCK-algebra
holds
(
X
is
BCK-positive-implicative
BCK-algebra
iff for
x
,
y
being
Element
of
X
holds
(
x
\
(
x
\
y
)
)
\
(
y
\
x
)
=
x
\
(
x
\
(
y
\
(
y
\
x
)
)
)
)
proof
end;
theorem
:: BCIALG_3:30
for
X
being
BCK-algebra
holds
(
X
is
BCK-positive-implicative
BCK-algebra
iff for
x
,
y
being
Element
of
X
holds
x
\
y
=
(
x
\
y
)
\
(
x
\
(
x
\
y
)
)
)
proof
end;
theorem
:: BCIALG_3:31
for
X
being
BCK-algebra
holds
(
X
is
BCK-positive-implicative
BCK-algebra
iff for
x
,
y
,
z
being
Element
of
X
holds
(
x
\
z
)
\
(
y
\
z
)
<=
(
x
\
y
)
\
z
)
proof
end;
theorem
:: BCIALG_3:32
for
X
being
BCK-algebra
holds
(
X
is
BCK-positive-implicative
BCK-algebra
iff for
x
,
y
being
Element
of
X
holds
x
\
y
<=
(
x
\
y
)
\
y
)
proof
end;
theorem
:: BCIALG_3:33
for
X
being
BCK-algebra
holds
(
X
is
BCK-positive-implicative
BCK-algebra
iff for
x
,
y
being
Element
of
X
holds
x
\
(
x
\
(
y
\
(
y
\
x
)
)
)
<=
(
x
\
(
x
\
y
)
)
\
(
y
\
x
)
)
proof
end;
theorem
Th34
:
:: BCIALG_3:34
for
X
being
BCK-algebra
holds
(
X
is
BCK-implicative
BCK-algebra
iff (
X
is
commutative
BCK-algebra
&
X
is
BCK-positive-implicative
BCK-algebra
) )
proof
end;
theorem
Th35
:
:: BCIALG_3:35
for
X
being
BCK-algebra
holds
(
X
is
BCK-implicative
BCK-algebra
iff for
x
,
y
being
Element
of
X
holds
(
x
\
(
x
\
y
)
)
\
(
x
\
y
)
=
y
\
(
y
\
x
)
)
proof
end;
theorem
:: BCIALG_3:36
for
X
being non
empty
BCIStr_0
holds
(
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
)
) )
proof
end;
Lm1
:
for
X
being
bounded
BCK-algebra
st
X
is
BCK-implicative
holds
for
a
being
Element
of
X
st
a
is
being_greatest
holds
for
x
being
Element
of
X
holds
a
\
(
a
\
x
)
=
x
proof
end;
theorem
Th37
:
:: BCIALG_3:37
for
X
being
bounded
BCK-algebra
for
a
being
Element
of
X
st
a
is
being_greatest
holds
(
X
is
BCK-implicative
iff (
X
is
involutory
&
X
is
BCK-positive-implicative
) )
proof
end;
theorem
:: BCIALG_3:38
for
X
being
BCK-algebra
holds
(
X
is
BCK-implicative
BCK-algebra
iff for
x
,
y
being
Element
of
X
holds
x
\
(
x
\
(
y
\
x
)
)
=
0.
X
)
proof
end;
theorem
:: BCIALG_3:39
for
X
being
BCK-algebra
holds
(
X
is
BCK-implicative
BCK-algebra
iff for
x
,
y
being
Element
of
X
holds
(
x
\
(
x
\
y
)
)
\
(
x
\
y
)
=
y
\
(
y
\
(
x
\
(
x
\
y
)
)
)
)
proof
end;
theorem
Th40
:
:: BCIALG_3:40
for
X
being
BCK-algebra
holds
(
X
is
BCK-implicative
BCK-algebra
iff for
x
,
y
,
z
being
Element
of
X
holds
(
x
\
z
)
\
(
x
\
y
)
=
(
y
\
z
)
\
(
(
y
\
x
)
\
z
)
)
proof
end;
theorem
:: BCIALG_3:41
for
X
being
BCK-algebra
holds
(
X
is
BCK-implicative
BCK-algebra
iff for
x
,
y
,
z
being
Element
of
X
holds
x
\
(
x
\
(
y
\
z
)
)
=
(
y
\
z
)
\
(
(
y
\
z
)
\
(
x
\
z
)
)
)
proof
end;
theorem
:: BCIALG_3:42
for
X
being
BCK-algebra
holds
(
X
is
BCK-implicative
BCK-algebra
iff for
x
,
y
being
Element
of
X
holds
x
\
(
x
\
y
)
=
(
y
\
(
y
\
x
)
)
\
(
x
\
y
)
)
proof
end;
theorem
Th43
:
:: BCIALG_3:43
for
X
being
commutative
bounded
BCK-algebra
for
a
being
Element
of
X
st
a
is
being_greatest
holds
(
X
is
BCK-implicative
iff for
x
being
Element
of
X
holds
(
a
\
x
)
\
(
(
a
\
x
)
\
x
)
=
0.
X
)
proof
end;
theorem
:: BCIALG_3:44
for
X
being
commutative
bounded
BCK-algebra
for
a
being
Element
of
X
st
a
is
being_greatest
holds
(
X
is
BCK-implicative
iff for
x
being
Element
of
X
holds
x
\
(
a
\
x
)
=
x
)
proof
end;
theorem
:: BCIALG_3:45
for
X
being
commutative
bounded
BCK-algebra
for
a
being
Element
of
X
st
a
is
being_greatest
holds
(
X
is
BCK-implicative
iff for
x
being
Element
of
X
holds
(
a
\
x
)
\
x
=
a
\
x
)
proof
end;
theorem
Th46
:
:: BCIALG_3:46
for
X
being
commutative
bounded
BCK-algebra
for
a
being
Element
of
X
st
a
is
being_greatest
holds
(
X
is
BCK-implicative
iff for
x
,
y
being
Element
of
X
holds
(
a
\
y
)
\
(
(
a
\
y
)
\
x
)
=
x
\
y
)
proof
end;
theorem
Th47
:
:: BCIALG_3:47
for
X
being
commutative
bounded
BCK-algebra
for
a
being
Element
of
X
st
a
is
being_greatest
holds
(
X
is
BCK-implicative
iff for
x
,
y
being
Element
of
X
holds
y
\
(
y
\
x
)
=
x
\
(
a
\
y
)
)
proof
end;
theorem
:: BCIALG_3:48
for
X
being
commutative
bounded
BCK-algebra
for
a
being
Element
of
X
st
a
is
being_greatest
holds
(
X
is
BCK-implicative
iff for
x
,
y
,
z
being
Element
of
X
holds
(
x
\
(
y
\
z
)
)
\
(
x
\
y
)
<=
x
\
(
a
\
z
)
)
proof
end;