begin
theorem
theorem
theorem
theorem
:: deftheorem defines initial_section BCIIDEAL:def 1 :
theorem Th5:
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines positive BCIIDEAL:def 2 :
theorem
theorem
theorem
begin
:: deftheorem Def3 defines associative BCIIDEAL:def 3 :
:: deftheorem Def4 defines associative-ideal BCIIDEAL:def 4 :
theorem
theorem Th15:
theorem
theorem
:: deftheorem Def5 defines p-ideal BCIIDEAL:def 5 :
theorem
theorem Th19:
theorem
theorem Th21:
theorem
begin
:: deftheorem Def6 defines commutative BCIIDEAL:def 6 :
theorem
theorem
Lm1:
for X being BCK-algebra holds the carrier of X c= BCK-part X
theorem Th25:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
:: deftheorem Def7 defines implicative-ideal BCIIDEAL:def 7 :
theorem Th50:
:: deftheorem Def8 defines positive-implicative-ideal BCIIDEAL:def 8 :
theorem Th51:
theorem Th52:
theorem Th53:
theorem
theorem
theorem
theorem