theorem Th50: :: BCIALG_5:50

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