let X be BCI-algebra; ( X is BCK-algebra of 1, 0 , 0 , 0 iff ( X is BCK-algebra of 0 , 0 , 0 , 0 & X is BCK-algebra of 0 ,1, 0 ,1 ) )
thus
( X is BCK-algebra of 1, 0 , 0 , 0 implies ( X is BCK-algebra of 0 , 0 , 0 , 0 & X is BCK-algebra of 0 ,1, 0 ,1 ) )
( X is BCK-algebra of 0 , 0 , 0 , 0 & X is BCK-algebra of 0 ,1, 0 ,1 implies X is BCK-algebra of 1, 0 , 0 , 0 )proof
assume
X is
BCK-algebra of 1,
0 ,
0 ,
0
;
( X is BCK-algebra of 0 , 0 , 0 , 0 & X is BCK-algebra of 0 ,1, 0 ,1 )
then
X is
BCK-implicative BCK-algebra
by Th50;
hence
(
X is
BCK-algebra of
0 ,
0 ,
0 ,
0 &
X is
BCK-algebra of
0 ,1,
0 ,1 )
by Th38, Th49;
verum
end;
assume
( X is BCK-algebra of 0 , 0 , 0 , 0 & X is BCK-algebra of 0 ,1, 0 ,1 )
; X is BCK-algebra of 1, 0 , 0 , 0
then
( X is commutative BCK-algebra & X is BCK-positive-implicative BCK-algebra )
by Th38, Th49;
then
X is BCK-implicative BCK-algebra
by BCIALG_3:34;
hence
X is BCK-algebra of 1, 0 , 0 , 0
by Th50; verum