theorem Th49: :: BCIALG_5:49

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