:: Orthomodular Lattices
:: by El\.zbieta M\c{a}dra and Adam Grabowski
::
:: Received June 27, 2008
:: Copyright (c) 2008 Association of Mizar Users
theorem Th1: :: ROBBINS4:1
theorem Th2: :: ROBBINS4:2
theorem Th3: :: ROBBINS4:3
theorem Th4: :: ROBBINS4:4
:: deftheorem Def1 defines orthomodular ROBBINS4:def 1 :
theorem Th5: :: ROBBINS4:5
theorem Th6: :: ROBBINS4:6
:: deftheorem Def2 defines Orthomodular ROBBINS4:def 2 :
definition
func B_6 -> RelStr equals :: ROBBINS4:def 3
InclPoset {0 ,1,(3 \ 1),2,(3 \ 2),3};
coherence
InclPoset {0 ,1,(3 \ 1),2,(3 \ 2),3} is RelStr
;
end;
:: deftheorem defines B_6 ROBBINS4:def 3 :
Lm1:
3 \ 2 misses 2
by XBOOLE_1:79;
Lm2:
1 c= 2
by NAT_1:40;
then Lm3:
3 \ 2 misses 1
by Lm1, XBOOLE_1:63;
theorem Th7: :: ROBBINS4:7
theorem Th8: :: ROBBINS4:8
:: deftheorem Def4 defines Benzene ROBBINS4:def 4 :
theorem Th9: :: ROBBINS4:9
theorem Th10: :: ROBBINS4:10
theorem Th11: :: ROBBINS4:11
theorem Th12: :: ROBBINS4:12
theorem Th13: :: ROBBINS4:13
theorem Th14: :: ROBBINS4:14
theorem Th15: :: ROBBINS4:15
theorem Th16: :: ROBBINS4:16
theorem Th17: :: ROBBINS4:17
theorem Th18: :: ROBBINS4:18
theorem Th19: :: ROBBINS4:19
theorem :: ROBBINS4:20
theorem Th21: :: ROBBINS4:21
theorem Th22: :: ROBBINS4:22
theorem Th23: :: ROBBINS4:23
for
a being
Element of
Benzene holds
( (
a = 0 implies
a ` = 3 ) & (
a = 3 implies
a ` = 0 ) & (
a = 1 implies
a ` = 3
\ 1 ) & (
a = 3
\ 1 implies
a ` = 1 ) & (
a = 2 implies
a ` = 3
\ 2 ) & (
a = 3
\ 2 implies
a ` = 2 ) )
theorem Th24: :: ROBBINS4:24
theorem Th25: :: ROBBINS4:25
theorem Th26: :: ROBBINS4:26
theorem Th27: :: ROBBINS4:27
theorem :: ROBBINS4:28
theorem Th29: :: ROBBINS4:29
:: deftheorem Def5 defines are_orthogonal ROBBINS4:def 5 :
theorem :: ROBBINS4:30
theorem :: ROBBINS4:31
theorem :: ROBBINS4:32
theorem :: ROBBINS4:33
theorem Th34: :: ROBBINS4:34
theorem :: ROBBINS4:35
theorem Th36: :: ROBBINS4:36
theorem :: ROBBINS4:37
theorem :: ROBBINS4:38
theorem :: ROBBINS4:39