begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
begin
:: deftheorem Def1 defines orthomodular ROBBINS4:def 1 :
theorem Th5:
theorem Th6:
:: deftheorem Def2 defines Orthomodular ROBBINS4:def 2 :
begin
definition
func B_6 -> RelStr equals
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:
theorem Th8:
:: deftheorem Def4 defines Benzene ROBBINS4:def 4 :
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem
theorem Th21:
theorem Th22:
theorem Th23:
for
a being
Element of 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:
theorem Th25:
theorem Th26:
theorem Th27:
theorem
theorem Th29:
begin
:: deftheorem Def5 defines are_orthogonal ROBBINS4:def 5 :
theorem
theorem
begin
theorem
theorem
theorem Th34:
theorem
theorem Th36:
theorem
theorem
theorem