:: Ideals of BCI-Algebras and Their Properties
:: by Chenglong Wu and Yuzhong Ding
::
:: Received March 3, 2008
:: Copyright (c) 2008 Association of Mizar Users
theorem :: BCIIDEAL:1
theorem :: BCIIDEAL:2
theorem :: BCIIDEAL:3
theorem :: BCIIDEAL:4
:: deftheorem defines initial_section BCIIDEAL:def 1 :
theorem Th5: :: BCIIDEAL:5
theorem :: BCIIDEAL:6
theorem :: BCIIDEAL:7
theorem :: BCIIDEAL:8
theorem :: BCIIDEAL:9
theorem :: BCIIDEAL:10
:: deftheorem defines positive BCIIDEAL:def 2 :
theorem :: BCIIDEAL:11
theorem :: BCIIDEAL:12
theorem :: BCIIDEAL:13
:: deftheorem Def3 defines associative BCIIDEAL:def 3 :
:: deftheorem Def4 defines associative-ideal BCIIDEAL:def 4 :
theorem :: BCIIDEAL:14
theorem Th15: :: BCIIDEAL:15
theorem :: BCIIDEAL:16
theorem :: BCIIDEAL:17
:: deftheorem Def5 defines p-ideal BCIIDEAL:def 5 :
theorem :: BCIIDEAL:18
theorem Th19: :: BCIIDEAL:19
theorem :: BCIIDEAL:20
theorem Th21: :: BCIIDEAL:21
theorem :: BCIIDEAL:22
:: deftheorem Def6 defines commutative BCIIDEAL:def 6 :
theorem :: BCIIDEAL:23
theorem :: BCIIDEAL:24
Lm1:
for X being BCK-algebra holds the carrier of X c= BCK-part X
theorem Th25: :: BCIIDEAL:25
theorem :: BCIIDEAL:26
theorem :: BCIIDEAL:27
theorem :: BCIIDEAL:28
theorem :: BCIIDEAL:29
theorem :: BCIIDEAL:30
theorem :: BCIIDEAL:31
theorem :: BCIIDEAL:32
theorem Th33: :: BCIIDEAL:33
theorem Th34: :: BCIIDEAL:34
theorem Th35: :: BCIIDEAL:35
theorem Th36: :: BCIIDEAL:36
theorem Th37: :: BCIIDEAL:37
theorem :: BCIIDEAL:38
theorem :: BCIIDEAL:39
theorem :: BCIIDEAL:40
theorem :: BCIIDEAL:41
theorem :: BCIIDEAL:42
theorem :: BCIIDEAL:43
theorem :: BCIIDEAL:44
theorem :: BCIIDEAL:45
theorem :: BCIIDEAL:46
theorem :: BCIIDEAL:47
theorem :: BCIIDEAL:48
theorem :: BCIIDEAL:49
:: deftheorem Def7 defines implicative-ideal BCIIDEAL:def 7 :
theorem Th50: :: BCIIDEAL:50
:: deftheorem Def8 defines positive-implicative-ideal BCIIDEAL:def 8 :
theorem Th51: :: BCIIDEAL:51
theorem Th52: :: BCIIDEAL:52
theorem Th53: :: BCIIDEAL:53
theorem :: BCIIDEAL:54
theorem :: BCIIDEAL:55
theorem :: BCIIDEAL:56
theorem :: BCIIDEAL:57