begin
:: deftheorem Def1 defines commutative BCIALG_3:def 1 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem
theorem Th8:
theorem
theorem
theorem
:: deftheorem Def2 defines being_greatest BCIALG_3:def 2 :
:: deftheorem defines being_positive BCIALG_3:def 3 :
begin
:: deftheorem Def4 defines BCI-commutative BCIALG_3:def 4 :
:: deftheorem Def5 defines BCI-weakly-commutative BCIALG_3:def 5 :
theorem
theorem
theorem
theorem
theorem Th16:
theorem Th17:
theorem
theorem
theorem
theorem
begin
:: deftheorem defines bounded BCIALG_3:def 6 :
:: deftheorem Def7 defines involutory BCIALG_3:def 7 :
theorem Th22:
theorem Th23:
theorem
:: deftheorem Def8 defines being_Iseki BCIALG_3:def 8 :
:: deftheorem defines Iseki_extension BCIALG_3:def 9 :
:: deftheorem Def10 defines Commutative-Ideal BCIALG_3:def 10 :
theorem
theorem Th26:
theorem
begin
:: deftheorem Def11 defines BCK-positive-implicative BCIALG_3:def 11 :
:: deftheorem Def12 defines BCK-implicative BCIALG_3:def 12 :
theorem Th28:
theorem Th29:
theorem
theorem
theorem
theorem
theorem Th34:
theorem Th35:
theorem
Lm1:
for X being bounded BCK-algebra st X is BCK-implicative holds
for a being Element of st a is being_greatest holds
for x being Element of holds a \ (a \ x) = x
theorem Th37:
theorem
theorem
theorem Th40:
theorem
theorem
theorem Th43:
theorem
theorem
theorem Th46:
theorem Th47:
theorem