let X be BCI-algebra; :: thesis: ( 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 )
:: thesis: ( X is BCK-algebra of 0 , 0 , 0 , 0 implies X is BCI-algebra of 0 , 0 , 0 , 0 )proof
assume B1:
X is
BCI-algebra of
0 ,
0 ,
0 ,
0
;
:: thesis: 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 Th39;
for
x,
y being
Element of
X holds
Polynom 0 ,
0 ,
x,
y = Polynom 0 ,
0 ,
y,
x
by B1, Def2;
hence
X is
BCK-algebra of
0 ,
0 ,
0 ,
0
by Def2;
:: thesis: verum
end;
thus
( X is BCK-algebra of 0 , 0 , 0 , 0 implies X is BCI-algebra of 0 , 0 , 0 , 0 )
; :: thesis: verum