let X be BCI-algebra; :: thesis: ( 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 ) ) :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum

end;

assume ( X is BCK-algebra of 0 , 0 , 0 , 0 & X is BCK-algebra of 0 ,1, 0 ,1 ) ; :: thesis: 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; :: thesis: verum