:: 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 P141: :: 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 Defzzz defines associative BCIIDEAL:def 3 :
:: deftheorem Def8 defines associative-ideal BCIIDEAL:def 4 :
theorem :: BCIIDEAL:14
theorem TL31321: :: BCIIDEAL:15
theorem :: BCIIDEAL:16
theorem :: BCIIDEAL:17
:: deftheorem Def1 defines p-ideal BCIIDEAL:def 5 :
theorem :: BCIIDEAL:18
theorem TL352: :: BCIIDEAL:19
theorem :: BCIIDEAL:20
theorem TL358: :: BCIIDEAL:21
theorem :: BCIIDEAL:22
:: deftheorem Def4 defines commutative BCIIDEAL:def 6 :
theorem :: BCIIDEAL:23
theorem :: BCIIDEAL:24
Lm3:
for X being BCK-algebra holds the carrier of X c= BCK-part X
theorem P25010: :: BCIIDEAL:25
theorem :: BCIIDEAL:26
theorem :: BCIIDEAL:27
theorem :: BCIIDEAL:28
theorem :: BCIIDEAL:29
theorem :: BCIIDEAL:30
theorem :: BCIIDEAL:31
theorem :: BCIIDEAL:32
theorem TL251: :: BCIIDEAL:33
theorem TL252: :: BCIIDEAL:34
theorem TL253: :: BCIIDEAL:35
theorem TL254: :: BCIIDEAL:36
theorem TL255: :: 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 Def2 defines implicative-ideal BCIIDEAL:def 7 :
theorem P351: :: BCIIDEAL:50
:: deftheorem Def5 defines positive-implicative-ideal BCIIDEAL:def 8 :
theorem TL341: :: BCIIDEAL:51
theorem TL3421: :: BCIIDEAL:52
theorem TL3422: :: BCIIDEAL:53
theorem :: BCIIDEAL:54
theorem :: BCIIDEAL:55
theorem :: BCIIDEAL:56
theorem :: BCIIDEAL:57