for X being BCI-algebra holds
( X is BCK-implicative BCK-algebra iff X is BCK-algebra of 1, 0 , 0 , 0 )