:: Several Classes of {BCK}-algebras and Their Properties
:: by Tao Sun , Dahai Hu and Xiquan Liang
::
:: Received September 19, 2007
:: Copyright (c) 2007 Association of Mizar Users
:: deftheorem Def1 defines commutative BCIALG_3:def 1 :
theorem Th1: :: BCIALG_3:1
theorem Th2: :: BCIALG_3:2
theorem Th3: :: BCIALG_3:3
theorem Th4: :: BCIALG_3:4
theorem Th5: :: BCIALG_3:5
theorem Th6: :: BCIALG_3:6
theorem :: BCIALG_3:7
theorem Th8: :: BCIALG_3:8
theorem :: BCIALG_3:9
theorem :: BCIALG_3:10
theorem :: BCIALG_3:11
:: deftheorem Def2 defines being_greatest BCIALG_3:def 2 :
:: deftheorem defines being_positive BCIALG_3:def 3 :
:: deftheorem Def4 defines BCI-commutative BCIALG_3:def 4 :
:: deftheorem Def5 defines BCI-weakly-commutative BCIALG_3:def 5 :
theorem :: BCIALG_3:12
theorem :: BCIALG_3:13
theorem :: BCIALG_3:14
theorem :: BCIALG_3:15
theorem Th16: :: BCIALG_3:16
theorem Th17: :: BCIALG_3:17
theorem :: BCIALG_3:18
theorem :: BCIALG_3:19
theorem :: BCIALG_3:20
theorem :: BCIALG_3:21
:: deftheorem defines bounded BCIALG_3:def 6 :
:: deftheorem Def7 defines involutory BCIALG_3:def 7 :
theorem Th22: :: BCIALG_3:22
theorem Th23: :: BCIALG_3:23
theorem :: BCIALG_3:24
:: 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 :: BCIALG_3:25
theorem Th26: :: BCIALG_3:26
theorem :: BCIALG_3:27
:: deftheorem Def11 defines BCK-positive-implicative BCIALG_3:def 11 :
:: deftheorem Def12 defines BCK-implicative BCIALG_3:def 12 :
theorem Th28: :: BCIALG_3:28
theorem Th29: :: BCIALG_3:29
theorem :: BCIALG_3:30
theorem :: BCIALG_3:31
theorem :: BCIALG_3:32
theorem :: BCIALG_3:33
theorem Th34: :: BCIALG_3:34
theorem Th35: :: BCIALG_3:35
theorem :: BCIALG_3:36
Lm1:
for X being bounded BCK-algebra st X is BCK-implicative holds
for a being Element of X st a is being_greatest holds
for x being Element of X holds a \ (a \ x) = x
theorem Th37: :: BCIALG_3:37
theorem :: BCIALG_3:38
theorem :: BCIALG_3:39
theorem Th40: :: BCIALG_3:40
theorem :: BCIALG_3:41
theorem :: BCIALG_3:42
theorem Th43: :: BCIALG_3:43
theorem :: BCIALG_3:44
theorem :: BCIALG_3:45
theorem Th46: :: BCIALG_3:46
theorem Th47: :: BCIALG_3:47
theorem :: BCIALG_3:48