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 Th47;
hence ( X is BCK-algebra of 0 , 0 , 0 , 0 & X is BCK-algebra of 0 ,1, 0 ,1 ) by Th46, Th41; :: thesis: verum

end;

assume A1: ( 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 A2: X is commutative BCK-algebra by Th41;
X is BCK-positive-implicative BCK-algebra by A1, Th46;
then X is BCK-implicative BCK-algebra by A2, BCIALG_3:34;
hence X is BCK-algebra of 1, 0 , 0 , 0 by Th47; :: thesis: verum