:: Axiomatization of {B}oolean Algebras Based on Sheffer Stroke
:: by Violetta Kozarkiewicz and Adam Grabowski
::
:: Received May 31, 2004
:: Copyright (c) 2004 Association of Mizar Users
theorem Th1: :: SHEFFER1:1
:: deftheorem Def1 defines upper-bounded' SHEFFER1:def 1 :
:: deftheorem Def2 defines Top' SHEFFER1:def 2 :
:: deftheorem Def3 defines lower-bounded' SHEFFER1:def 3 :
:: deftheorem Def4 defines Bot' SHEFFER1:def 4 :
:: deftheorem Def5 defines distributive' SHEFFER1:def 5 :
:: deftheorem Def6 defines is_a_complement'_of SHEFFER1:def 6 :
:: deftheorem Def7 defines complemented' SHEFFER1:def 7 :
:: deftheorem Def8 defines `# SHEFFER1:def 8 :
theorem :: SHEFFER1:2
canceled;
theorem Th3: :: SHEFFER1:3
theorem Th4: :: SHEFFER1:4
theorem Th5: :: SHEFFER1:5
theorem Th6: :: SHEFFER1:6
theorem Th7: :: SHEFFER1:7
theorem Th8: :: SHEFFER1:8
:: deftheorem Def9 defines meet-idempotent SHEFFER1:def 9 :
theorem Th9: :: SHEFFER1:9
theorem Th10: :: SHEFFER1:10
theorem Th11: :: SHEFFER1:11
theorem Th12: :: SHEFFER1:12
theorem Th13: :: SHEFFER1:13
theorem Th14: :: SHEFFER1:14
theorem Th15: :: SHEFFER1:15
theorem Th16: :: SHEFFER1:16
theorem Th17: :: SHEFFER1:17
theorem Th18: :: SHEFFER1:18
theorem Th19: :: SHEFFER1:19
theorem Th20: :: SHEFFER1:20
theorem Th21: :: SHEFFER1:21
theorem Th22: :: SHEFFER1:22
theorem :: SHEFFER1:23
theorem Th24: :: SHEFFER1:24
theorem Th25: :: SHEFFER1:25
theorem Th26: :: SHEFFER1:26
:: deftheorem defines TrivShefferOrthoLattStr SHEFFER1:def 10 :
:: deftheorem defines | SHEFFER1:def 11 :
:: deftheorem Def12 defines properly_defined SHEFFER1:def 12 :
:: deftheorem Def13 defines satisfying_Sheffer_1 SHEFFER1:def 13 :
:: deftheorem Def14 defines satisfying_Sheffer_2 SHEFFER1:def 14 :
:: deftheorem Def15 defines satisfying_Sheffer_3 SHEFFER1:def 15 :
theorem :: SHEFFER1:27
theorem :: SHEFFER1:28
theorem :: SHEFFER1:29
:: deftheorem defines " SHEFFER1:def 16 :
theorem :: SHEFFER1:30
theorem :: SHEFFER1:31
theorem Th32: :: SHEFFER1:32
theorem Th33: :: SHEFFER1:33
theorem Th34: :: SHEFFER1:34
theorem Th35: :: SHEFFER1:35
theorem Th36: :: SHEFFER1:36
theorem Th37: :: SHEFFER1:37
theorem :: SHEFFER1:38