:: ROBBINS4 semantic presentation begin registrationlet "L" be ($#l3_lattices :::"Lattice":::); cluster (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" "L") "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" "L") "#)" ) -> ($#v10_lattices :::"Lattice-like"::: ) ; end; theorem :: ROBBINS4:1 (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "being" ($#l3_lattices :::"Lattice":::) "st" (Bool (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "K"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "L"))) "#)" ))) "holds" (Bool (Set ($#k3_lattice3 :::"LattPOSet"::: ) (Set (Var "K"))) ($#r1_hidden :::"="::: ) (Set ($#k3_lattice3 :::"LattPOSet"::: ) (Set (Var "L"))))) ; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v3_robbins3 :::"meet-Absorbing"::: ) for ($#l4_robbins1 :::"OrthoLattStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v10_robbins1 :::"de_Morgan"::: ) ($#v8_robbins3 :::"involutive"::: ) ($#v9_robbins3 :::"with_Top"::: ) -> ($#v13_lattices :::"lower-bounded"::: ) for ($#l4_robbins1 :::"OrthoLattStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v10_robbins1 :::"de_Morgan"::: ) ($#v8_robbins3 :::"involutive"::: ) ($#v9_robbins3 :::"with_Top"::: ) -> ($#v14_lattices :::"upper-bounded"::: ) for ($#l4_robbins1 :::"OrthoLattStr"::: ) ; end; theorem :: ROBBINS4:2 (Bool "for" (Set (Var "L")) "being" ($#l4_robbins1 :::"Ortholattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L")))) & (Bool (Set (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L")))) ")" ))) ; theorem :: ROBBINS4:3 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_robbins1 :::"OrthoLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#l4_robbins1 :::"Ortholattice":::)) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "b")) ")" ) ($#k1_lattices :::""\/""::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "c")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k2_lattices :::""/\""::: ) (Set "(" (Set (Var "b")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::""\/""::: ) (Set (Var "a")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k2_lattices :::""/\""::: ) (Set "(" (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "b")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set "(" (Set (Var "b")) ($#k2_lattices :::""/\""::: ) (Set "(" (Set (Var "b")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ))) ")" ) ")" ) ")" )) ; theorem :: ROBBINS4:4 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v8_robbins3 :::"involutive"::: ) ($#l4_robbins1 :::"OrthoLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v10_robbins1 :::"de_Morgan"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "b")) ($#k3_robbins1 :::"`"::: ) ) ($#r3_lattices :::"[="::: ) (Set (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ))) ")" )) ; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_robbins1 :::"OrthoLattStr"::: ) ; attr "L" is :::"orthomodular"::: means :: ROBBINS4:def 1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool (Set (Var "x")) ($#r1_lattices :::"[="::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_lattices :::""\/""::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k2_lattices :::""/\""::: ) (Set (Var "y")) ")" )))); end; :: deftheorem defines :::"orthomodular"::: ROBBINS4:def 1 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_robbins1 :::"OrthoLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_robbins4 :::"orthomodular"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_lattices :::"[="::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_lattices :::""\/""::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k2_lattices :::""/\""::: ) (Set (Var "y")) ")" )))) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_struct_0 :::"trivial"::: ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v7_lattices :::"meet-associative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#v10_lattices :::"Lattice-like"::: ) ($#v12_lattices :::"modular"::: ) ($#v13_lattices :::"lower-bounded"::: ) ($#v14_lattices :::"upper-bounded"::: ) bbbadV15_LATTICES() ($#v17_lattices :::"Boolean"::: ) ($#v10_robbins1 :::"de_Morgan"::: ) ($#v1_robbins3 :::"join-Associative"::: ) ($#v2_robbins3 :::"meet-Associative"::: ) ($#v3_robbins3 :::"meet-Absorbing"::: ) ($#v8_robbins3 :::"involutive"::: ) ($#v9_robbins3 :::"with_Top"::: ) ($#v1_robbins4 :::"orthomodular"::: ) for ($#l4_robbins1 :::"OrthoLattStr"::: ) ; end; theorem :: ROBBINS4:5 (Bool "for" (Set (Var "L")) "being" ($#v12_lattices :::"modular"::: ) ($#l4_robbins1 :::"Ortholattice":::) "holds" (Bool (Set (Var "L")) "is" ($#v1_robbins4 :::"orthomodular"::: ) )) ; definitionmode Orthomodular_Lattice is ($#v1_robbins4 :::"orthomodular"::: ) ($#l4_robbins1 :::"Ortholattice":::); end; theorem :: ROBBINS4:6 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_lattices :::"join-associative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#v1_robbins4 :::"orthomodular"::: ) ($#l4_robbins1 :::"OrthoLattStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "x")) ($#k1_lattices :::""\/""::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k4_lattices :::""/\""::: ) (Set "(" (Set (Var "x")) ($#k1_lattices :::""\/""::: ) (Set (Var "y")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_lattices :::""\/""::: ) (Set (Var "y")))))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_robbins1 :::"OrthoLattStr"::: ) ; attr "L" is :::"Orthomodular"::: means :: ROBBINS4:def 2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set (Set (Var "x")) ($#k1_lattices :::""\/""::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k2_lattices :::""/\""::: ) (Set "(" (Set (Var "x")) ($#k1_lattices :::""\/""::: ) (Set (Var "y")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_lattices :::""\/""::: ) (Set (Var "y"))))); end; :: deftheorem defines :::"Orthomodular"::: ROBBINS4:def 2 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_robbins1 :::"OrthoLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v2_robbins4 :::"Orthomodular"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "x")) ($#k1_lattices :::""\/""::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k2_lattices :::""/\""::: ) (Set "(" (Set (Var "x")) ($#k1_lattices :::""\/""::: ) (Set (Var "y")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_lattices :::""\/""::: ) (Set (Var "y"))))) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_lattices :::"join-associative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#v2_robbins4 :::"Orthomodular"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_lattices :::"join-associative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#v1_robbins4 :::"orthomodular"::: ) for ($#l4_robbins1 :::"OrthoLattStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_lattices :::"join-associative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#v1_robbins4 :::"orthomodular"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_lattices :::"join-associative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#v2_robbins4 :::"Orthomodular"::: ) for ($#l4_robbins1 :::"OrthoLattStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v12_lattices :::"modular"::: ) ($#v10_robbins1 :::"de_Morgan"::: ) ($#v8_robbins3 :::"involutive"::: ) ($#v9_robbins3 :::"with_Top"::: ) -> ($#v1_robbins4 :::"orthomodular"::: ) for ($#l4_robbins1 :::"OrthoLattStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_lattices :::"join-commutative"::: ) ($#v5_lattices :::"join-associative"::: ) ($#v6_lattices :::"meet-commutative"::: ) ($#v7_lattices :::"meet-associative"::: ) ($#v8_lattices :::"meet-absorbing"::: ) ($#v9_lattices :::"join-absorbing"::: ) ($#v10_lattices :::"Lattice-like"::: ) ($#v13_lattices :::"lower-bounded"::: ) ($#v14_lattices :::"upper-bounded"::: ) bbbadV15_LATTICES() ($#v10_robbins1 :::"de_Morgan"::: ) ($#v1_robbins3 :::"join-Associative"::: ) ($#v2_robbins3 :::"meet-Associative"::: ) ($#v3_robbins3 :::"meet-Absorbing"::: ) ($#v8_robbins3 :::"involutive"::: ) ($#v9_robbins3 :::"with_Top"::: ) ($#v1_robbins4 :::"orthomodular"::: ) for ($#l4_robbins1 :::"OrthoLattStr"::: ) ; end; begin definitionfunc :::"B_6"::: -> ($#l1_orders_2 :::"RelStr"::: ) equals :: ROBBINS4:def 3 (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set ($#k4_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set "(" (Num 3) ($#k6_subset_1 :::"\"::: ) (Num 1) ")" ) "," (Num 2) "," (Set "(" (Num 3) ($#k6_subset_1 :::"\"::: ) (Num 2) ")" ) "," (Num 3) ($#k4_enumset1 :::"}"::: ) )); end; :: deftheorem defines :::"B_6"::: ROBBINS4:def 3 : (Bool (Set ($#k1_robbins4 :::"B_6"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set ($#k4_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set "(" (Num 3) ($#k6_subset_1 :::"\"::: ) (Num 1) ")" ) "," (Num 2) "," (Set "(" (Num 3) ($#k6_subset_1 :::"\"::: ) (Num 2) ")" ) "," (Num 3) ($#k4_enumset1 :::"}"::: ) ))); registration cluster (Set ($#k1_robbins4 :::"B_6"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; cluster (Set ($#k1_robbins4 :::"B_6"::: ) ) -> ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ; end; registration cluster (Set ($#k1_robbins4 :::"B_6"::: ) ) -> ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ; end; theorem :: ROBBINS4:7 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k14_lattice3 :::"latt"::: ) (Set ($#k1_robbins4 :::"B_6"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set "(" (Num 3) ($#k6_subset_1 :::"\"::: ) (Num 1) ")" ) "," (Num 2) "," (Set "(" (Num 3) ($#k6_subset_1 :::"\"::: ) (Num 2) ")" ) "," (Num 3) ($#k4_enumset1 :::"}"::: ) )) ; theorem :: ROBBINS4:8 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k14_lattice3 :::"latt"::: ) (Set ($#k1_robbins4 :::"B_6"::: ) ) ")" )))) "holds" (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Num 3))) ; definitionfunc :::"Benzene"::: -> ($#v4_robbins1 :::"strict"::: ) ($#l4_robbins1 :::"OrthoLattStr"::: ) means :: ROBBINS4:def 4 (Bool "(" (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" it) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" it) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k14_lattice3 :::"latt"::: ) (Set ($#k1_robbins4 :::"B_6"::: ) ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" it (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Num 3) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" it) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k3_subset_1 :::"`"::: ) ))) ")" ) ")" ); end; :: deftheorem defines :::"Benzene"::: ROBBINS4:def 4 : (Bool "for" (Set (Var "b1")) "being" ($#v4_robbins1 :::"strict"::: ) ($#l4_robbins1 :::"OrthoLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k2_robbins4 :::"Benzene"::: ) )) "iff" (Bool "(" (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b1"))) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set (Var "b1"))) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set (Var "b1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k14_lattice3 :::"latt"::: ) (Set ($#k1_robbins4 :::"B_6"::: ) ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "b1")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Num 3) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" (Set (Var "b1"))) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k3_subset_1 :::"`"::: ) ))) ")" ) ")" ) ")" )); theorem :: ROBBINS4:9 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k2_robbins4 :::"Benzene"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set "(" (Num 3) ($#k6_subset_1 :::"\"::: ) (Num 1) ")" ) "," (Num 2) "," (Set "(" (Num 3) ($#k6_subset_1 :::"\"::: ) (Num 2) ")" ) "," (Num 3) ($#k4_enumset1 :::"}"::: ) )) ; theorem :: ROBBINS4:10 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k2_robbins4 :::"Benzene"::: ) )) ($#r1_tarski :::"c="::: ) (Set ($#k1_zfmisc_1 :::"bool"::: ) (Num 3))) ; theorem :: ROBBINS4:11 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k2_robbins4 :::"Benzene"::: ) )))) "holds" (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) ))) ; registration cluster (Set ($#k2_robbins4 :::"Benzene"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_robbins1 :::"strict"::: ) ; cluster (Set ($#k2_robbins4 :::"Benzene"::: ) ) -> ($#v10_lattices :::"Lattice-like"::: ) ($#v4_robbins1 :::"strict"::: ) ; end; theorem :: ROBBINS4:12 (Bool (Set ($#k3_lattice3 :::"LattPOSet"::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k2_robbins4 :::"Benzene"::: ) )) "," (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set ($#k2_robbins4 :::"Benzene"::: ) )) "," (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set ($#k2_robbins4 :::"Benzene"::: ) )) "#)" )) ($#r1_hidden :::"="::: ) (Set ($#k1_robbins4 :::"B_6"::: ) )) ; theorem :: ROBBINS4:13 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_robbins4 :::"B_6"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k2_robbins4 :::"Benzene"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r3_orders_2 :::"<="::: ) (Set (Var "b"))) "iff" (Bool (Set (Var "x")) ($#r3_lattices :::"[="::: ) (Set (Var "y"))) ")" ))) ; theorem :: ROBBINS4:14 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_robbins4 :::"B_6"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k2_robbins4 :::"Benzene"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_lattices :::""\/""::: ) (Set (Var "y")))) & (Bool (Set (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_lattices :::""/\""::: ) (Set (Var "y")))) ")" ))) ; theorem :: ROBBINS4:15 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_robbins4 :::"B_6"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Num 3) ($#k6_subset_1 :::"\"::: ) (Num 1))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Num 2))) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Num 3)) & (Bool (Set (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: ROBBINS4:16 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_robbins4 :::"B_6"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Num 3) ($#k6_subset_1 :::"\"::: ) (Num 2))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Num 3)) & (Bool (Set (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: ROBBINS4:17 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_robbins4 :::"B_6"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Num 3) ($#k6_subset_1 :::"\"::: ) (Num 1))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Num 3)) & (Bool (Set (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: ROBBINS4:18 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_robbins4 :::"B_6"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Num 3) ($#k6_subset_1 :::"\"::: ) (Num 2))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Num 2))) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Num 3)) & (Bool (Set (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: ROBBINS4:19 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k2_robbins4 :::"Benzene"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Num 3) ($#k6_subset_1 :::"\"::: ) (Num 1))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Num 2))) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Num 3)) & (Bool (Set (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: ROBBINS4:20 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k2_robbins4 :::"Benzene"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Num 3) ($#k6_subset_1 :::"\"::: ) (Num 2))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Num 3))) ; theorem :: ROBBINS4:21 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k2_robbins4 :::"Benzene"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Num 3) ($#k6_subset_1 :::"\"::: ) (Num 1))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Num 3))) ; theorem :: ROBBINS4:22 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k2_robbins4 :::"Benzene"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Num 3) ($#k6_subset_1 :::"\"::: ) (Num 2))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Num 2))) "holds" (Bool (Set (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Num 3))) ; theorem :: ROBBINS4:23 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k2_robbins4 :::"Benzene"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Num 3)) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Num 3))) "implies" (Bool (Set (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Num 1))) "implies" (Bool (Set (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Num 3) ($#k6_subset_1 :::"\"::: ) (Num 1))) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Num 3) ($#k6_subset_1 :::"\"::: ) (Num 1)))) "implies" (Bool (Set (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Num 2))) "implies" (Bool (Set (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Num 3) ($#k6_subset_1 :::"\"::: ) (Num 2))) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Num 3) ($#k6_subset_1 :::"\"::: ) (Num 2)))) "implies" (Bool (Set (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Num 2)) ")" ")" )) ; theorem :: ROBBINS4:24 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k2_robbins4 :::"Benzene"::: ) ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Var "b"))) "iff" (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set (Var "b"))) ")" )) ; theorem :: ROBBINS4:25 (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k2_robbins4 :::"Benzene"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ; theorem :: ROBBINS4:26 (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k2_robbins4 :::"Benzene"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ; theorem :: ROBBINS4:27 (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k2_robbins4 :::"Benzene"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Num 3))) "holds" (Bool (Set (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ; registration cluster (Set ($#k2_robbins4 :::"Benzene"::: ) ) -> ($#v13_lattices :::"lower-bounded"::: ) ($#v4_robbins1 :::"strict"::: ) ; cluster (Set ($#k2_robbins4 :::"Benzene"::: ) ) -> ($#v14_lattices :::"upper-bounded"::: ) ($#v4_robbins1 :::"strict"::: ) ; end; theorem :: ROBBINS4:28 (Bool (Set ($#k6_lattices :::"Top"::: ) (Set ($#k2_robbins4 :::"Benzene"::: ) )) ($#r1_hidden :::"="::: ) (Num 3)) ; theorem :: ROBBINS4:29 (Bool (Set ($#k5_lattices :::"Bottom"::: ) (Set ($#k2_robbins4 :::"Benzene"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ; registration cluster (Set ($#k2_robbins4 :::"Benzene"::: ) ) -> ($#v4_robbins1 :::"strict"::: ) ($#v10_robbins1 :::"de_Morgan"::: ) ($#v8_robbins3 :::"involutive"::: ) ($#v9_robbins3 :::"with_Top"::: ) ; cluster (Set ($#k2_robbins4 :::"Benzene"::: ) ) -> ($#v4_robbins1 :::"strict"::: ) ($#~v1_robbins4 "non" ($#v1_robbins4 :::"orthomodular"::: ) ) ; end; begin definitionlet "L" be ($#l4_robbins1 :::"Ortholattice":::); let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); pred "a" "," "b" :::"are_orthogonal"::: means :: ROBBINS4:def 5 (Bool "a" ($#r3_lattices :::"[="::: ) (Set "b" ($#k3_robbins1 :::"`"::: ) )); end; :: deftheorem defines :::"are_orthogonal"::: ROBBINS4:def 5 : (Bool "for" (Set (Var "L")) "being" ($#l4_robbins1 :::"Ortholattice":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_robbins4 :::"are_orthogonal"::: ) ) "iff" (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Set (Var "b")) ($#k3_robbins1 :::"`"::: ) )) ")" ))); notationlet "L" be ($#l4_robbins1 :::"Ortholattice":::); let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); synonym "a" :::"_|_"::: "b" for "a" "," "b" :::"are_orthogonal"::: ; end; theorem :: ROBBINS4:30 (Bool "for" (Set (Var "L")) "being" ($#l4_robbins1 :::"Ortholattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_robbins4 :::"_|_"::: ) (Set (Var "a"))) "iff" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L")))) ")" ))) ; definitionlet "L" be ($#l4_robbins1 :::"Ortholattice":::); let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); :: original: :::"are_orthogonal"::: redefine pred "a" "," "b" :::"are_orthogonal"::: ; symmetry (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")) "st" (Bool (Bool ((Set (Const "L")) "," (Set (Var "b1")) "," (Set (Var "b2"))))) "holds" (Bool ((Set (Const "L")) "," (Set (Var "b2")) "," (Set (Var "b1"))))) ; end; theorem :: ROBBINS4:31 (Bool "for" (Set (Var "L")) "being" ($#l4_robbins1 :::"Ortholattice":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r1_robbins4 :::"_|_"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r1_robbins4 :::"_|_"::: ) (Set (Var "c")))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_robbins4 :::"_|_"::: ) (Set (Set (Var "b")) ($#k4_lattices :::""/\""::: ) (Set (Var "c")))) & (Bool (Set (Var "a")) ($#r1_robbins4 :::"_|_"::: ) (Set (Set (Var "b")) ($#k3_lattices :::""\/""::: ) (Set (Var "c")))) ")" ))) ; begin theorem :: ROBBINS4:32 (Bool "for" (Set (Var "L")) "being" ($#l4_robbins1 :::"Ortholattice":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_robbins4 :::"orthomodular"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Set (Var "b")) ($#k3_robbins1 :::"`"::: ) ) ($#r3_lattices :::"[="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "L"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k3_robbins1 :::"`"::: ) ))) ")" )) ; theorem :: ROBBINS4:33 (Bool "for" (Set (Var "L")) "being" ($#l4_robbins1 :::"Ortholattice":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_robbins4 :::"orthomodular"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r1_robbins4 :::"_|_"::: ) (Set (Var "b"))) & (Bool (Set (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "L"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k3_robbins1 :::"`"::: ) ))) ")" )) ; theorem :: ROBBINS4:34 (Bool "for" (Set (Var "L")) "being" ($#l4_robbins1 :::"Ortholattice":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_robbins4 :::"orthomodular"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "b")) ($#r3_lattices :::"[="::: ) (Set (Var "a")))) "holds" (Bool (Set (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k3_lattices :::""\/""::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ")" )) ; theorem :: ROBBINS4:35 (Bool "for" (Set (Var "L")) "being" ($#l4_robbins1 :::"Ortholattice":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_robbins4 :::"orthomodular"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k3_lattices :::""\/""::: ) (Set "(" (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set (Var "b")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set (Var "b"))))) ")" )) ; theorem :: ROBBINS4:36 (Bool "for" (Set (Var "L")) "being" ($#l4_robbins1 :::"Ortholattice":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_robbins4 :::"orthomodular"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "b")) ")" ) ($#k4_lattices :::""/\""::: ) (Set (Var "a")) ")" ) ($#k3_lattices :::""\/""::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "b")) ")" ) ($#k4_lattices :::""/\""::: ) (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" )))) ")" )) ; theorem :: ROBBINS4:37 (Bool "for" (Set (Var "L")) "being" ($#l4_robbins1 :::"Ortholattice":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_robbins4 :::"orthomodular"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r3_lattices :::"[="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "b")) ")" ) ($#k4_lattices :::""/\""::: ) (Set "(" (Set (Var "b")) ($#k3_lattices :::""\/""::: ) (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set (Var "b")) ")" ) ($#k3_lattices :::""\/""::: ) (Set "(" (Set (Var "b")) ($#k4_lattices :::""/\""::: ) (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" )))) ")" )) ; theorem :: ROBBINS4:38 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_robbins1 :::"OrthoLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#l4_robbins1 :::"Orthomodular_Lattice":::)) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "b")) ")" ) ($#k1_lattices :::""\/""::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "c")) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k2_lattices :::""/\""::: ) (Set "(" (Set (Var "b")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ) ($#k3_robbins1 :::"`"::: ) ")" ) ($#k1_lattices :::""\/""::: ) (Set (Var "a")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "b")) ")" ) ($#k2_lattices :::""/\""::: ) (Set "(" (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "c")) ")" ) ")" ) ($#k1_lattices :::""\/""::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set (Var "b")) ")" ) ($#k2_lattices :::""/\""::: ) (Set "(" (Set (Var "a")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_lattices :::""\/""::: ) (Set "(" (Set (Var "b")) ($#k2_lattices :::""/\""::: ) (Set "(" (Set (Var "b")) ($#k3_robbins1 :::"`"::: ) ")" ) ")" ))) ")" ) ")" ) ")" )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v10_robbins1 :::"de_Morgan"::: ) ($#v1_robbins3 :::"join-Associative"::: ) ($#v3_robbins3 :::"meet-Absorbing"::: ) ($#v1_robbins4 :::"orthomodular"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_lattices :::"Lattice-like"::: ) ($#v10_robbins1 :::"de_Morgan"::: ) ($#v1_robbins3 :::"join-Associative"::: ) ($#v3_robbins3 :::"meet-Absorbing"::: ) ($#v9_robbins3 :::"with_Top"::: ) ($#v1_robbins4 :::"orthomodular"::: ) for ($#l4_robbins1 :::"OrthoLattStr"::: ) ; end; theorem :: ROBBINS4:39 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_robbins1 :::"OrthoLattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#l4_robbins1 :::"Orthomodular_Lattice":::)) "iff" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_robbins3 :::"join-Associative"::: ) ) & (Bool (Set (Var "L")) "is" ($#v3_robbins3 :::"meet-Absorbing"::: ) ) & (Bool (Set (Var "L")) "is" ($#v10_robbins1 :::"de_Morgan"::: ) ) & (Bool (Set (Var "L")) "is" ($#v2_robbins4 :::"Orthomodular"::: ) ) ")" ) ")" )) ;