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 )

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

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

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