theorem Th25: :: BCIIDEAL:25

for X being BCK-algebra holds BCK-part X = the carrier of X by Lm1;