theorem Th19: :: BCIALG_1:19

for X being BCI-algebra holds 0. X in BCK-part X