let X be BCI-algebra; ( X is BCI-algebra of 0 , 0 , 0 , 0 iff X is BCK-algebra of 0 , 0 , 0 , 0 )
thus
( X is BCI-algebra of 0 , 0 , 0 , 0 implies X is BCK-algebra of 0 , 0 , 0 , 0 )
( X is BCK-algebra of 0 , 0 , 0 , 0 implies X is BCI-algebra of 0 , 0 , 0 , 0 )proof
assume A1:
X is
BCI-algebra of
0 ,
0 ,
0 ,
0
;
X is BCK-algebra of 0 , 0 , 0 , 0
then
X is
BCI-algebra of
0 ,
0 ,
0 + 0,
0 + 0
;
then reconsider X =
X as
BCK-algebra by Th36;
for
x,
y being
Element of
X holds
Polynom (
0,
0,
x,
y)
= Polynom (
0,
0,
y,
x)
by A1, Def3;
hence
X is
BCK-algebra of
0 ,
0 ,
0 ,
0
by Def3;
verum
end;
thus
( X is BCK-algebra of 0 , 0 , 0 , 0 implies X is BCI-algebra of 0 , 0 , 0 , 0 )
; verum