:: YELLOW_5 semantic presentation begin theorem :: YELLOW_5:1 (Bool "for" (Set (Var "L")) "being" ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: YELLOW_5:2 (Bool "for" (Set (Var "L")) "being" ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: YELLOW_5:3 (Bool "for" (Set (Var "L")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b"))) ($#r1_orders_2 :::"<="::: ) (Set (Var "c")))) "holds" (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "c"))))) ; theorem :: YELLOW_5:4 (Bool "for" (Set (Var "L")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) (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 "c")) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "c")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a"))))) ; theorem :: YELLOW_5:5 (Bool "for" (Set (Var "L")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) (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")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b"))) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "c")))))) ; theorem :: YELLOW_5:6 (Bool "for" (Set (Var "L")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) (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_orders_2 :::"<="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "c"))) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "b")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "c")))))) ; theorem :: YELLOW_5:7 (Bool "for" (Set (Var "L")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) (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_orders_2 :::"<="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "c"))) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "b")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "c")))))) ; theorem :: YELLOW_5:8 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r3_orders_2 :::"<="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: YELLOW_5:9 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"sup-Semilattice":::) (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")) ($#r3_orders_2 :::"<="::: ) (Set (Var "c"))) & (Bool (Set (Var "b")) ($#r3_orders_2 :::"<="::: ) (Set (Var "c")))) "holds" (Bool (Set (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b"))) ($#r3_orders_2 :::"<="::: ) (Set (Var "c"))))) ; theorem :: YELLOW_5:10 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "b")) ($#r3_orders_2 :::"<="::: ) (Set (Var "a")))) "holds" (Bool (Set (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; begin theorem :: YELLOW_5:11 (Bool "for" (Set (Var "L")) "being" ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r6_waybel_1 :::"is_a_complement_of"::: ) (Set (Var "x"))) "iff" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "x")))) ")" ))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func "a" :::"\"::: "b" -> ($#m1_subset_1 :::"Element":::) "of" "L" equals :: YELLOW_5:def 1 (Set "a" ($#k11_lattice3 :::""/\""::: ) (Set "(" ($#k7_waybel_1 :::"'not'"::: ) "b" ")" )); end; :: deftheorem defines :::"\"::: YELLOW_5:def 1 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k11_lattice3 :::""/\""::: ) (Set "(" ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "b")) ")" ))))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func "a" :::"\+\"::: "b" -> ($#m1_subset_1 :::"Element":::) "of" "L" equals :: YELLOW_5:def 2 (Set (Set "(" "a" ($#k1_yellow_5 :::"\"::: ) "b" ")" ) ($#k10_lattice3 :::""\/""::: ) (Set "(" "b" ($#k1_yellow_5 :::"\"::: ) "a" ")" )); end; :: deftheorem defines :::"\+\"::: YELLOW_5:def 2 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k2_yellow_5 :::"\+\"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "b")) ")" ) ($#k10_lattice3 :::""\/""::: ) (Set "(" (Set (Var "b")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "a")) ")" ))))); definitionlet "L" be ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); :: original: :::"\+\"::: redefine func "a" :::"\+\"::: "b" -> ($#m1_subset_1 :::"Element":::) "of" "L"; commutativity (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")) "holds" (Bool (Set (Set (Var "a")) ($#k2_yellow_5 :::"\+\"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k2_yellow_5 :::"\+\"::: ) (Set (Var "a"))))) ; end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); pred "a" :::"meets"::: "b" means :: YELLOW_5:def 3 (Bool (Set "a" ($#k11_lattice3 :::""/\""::: ) "b") ($#r1_hidden :::"<>"::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) "L")); end; :: deftheorem defines :::"meets"::: YELLOW_5:def 3 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_yellow_5 :::"meets"::: ) (Set (Var "b"))) "iff" (Bool (Set (Set (Var "a")) ($#k11_lattice3 :::""/\""::: ) (Set (Var "b"))) ($#r1_hidden :::"<>"::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")))) ")" ))); notationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); antonym "a" :::"misses"::: "b" for "a" :::"meets"::: "b"; end; notationlet "L" be ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); antonym "a" :::"misses"::: "b" for "a" :::"meets"::: "b"; end; definitionlet "L" be ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); :: original: :::"meets"::: redefine pred "a" :::"meets"::: "b"; 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 :: YELLOW_5:12 (Bool "for" (Set (Var "L")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) (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_orders_2 :::"<="::: ) (Set (Var "c")))) "holds" (Bool (Set (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "b"))) ($#r1_orders_2 :::"<="::: ) (Set (Var "c"))))) ; theorem :: YELLOW_5:13 (Bool "for" (Set (Var "L")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) (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_orders_2 :::"<="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "c"))) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "b")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "c")))))) ; theorem :: YELLOW_5:14 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "b"))) ($#r3_orders_2 :::"<="::: ) (Set (Var "c"))) & (Bool (Set (Set (Var "b")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "a"))) ($#r3_orders_2 :::"<="::: ) (Set (Var "c")))) "holds" (Bool (Set (Set (Var "a")) ($#k3_yellow_5 :::"\+\"::: ) (Set (Var "b"))) ($#r3_orders_2 :::"<="::: ) (Set (Var "c"))))) ; theorem :: YELLOW_5:15 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_yellow_5 :::"meets"::: ) (Set (Var "a"))) "iff" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")))) ")" ))) ; theorem :: YELLOW_5:16 (Bool "for" (Set (Var "L")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "L")) "is" ($#v2_waybel_1 :::"distributive"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Set "(" (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b")) ")" ) ($#k10_lattice3 :::""\/""::: ) (Set "(" (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "b")) ($#k10_lattice3 :::""\/""::: ) (Set (Var "c")))))) ; theorem :: YELLOW_5:17 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set (Var "L")) "is" ($#v2_waybel_1 :::"distributive"::: ) )) "holds" (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")) ($#k13_lattice3 :::""\/""::: ) (Set "(" (Set (Var "b")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b")) ")" ) ($#k12_lattice3 :::""/\""::: ) (Set "(" (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "c")) ")" ))))) ; theorem :: YELLOW_5:18 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"LATTICE":::) "st" (Bool (Bool (Set (Var "L")) "is" ($#v2_waybel_1 :::"distributive"::: ) )) "holds" (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")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b")) ")" ) ($#k1_yellow_5 :::"\"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "c")) ")" ) ($#k13_lattice3 :::""\/""::: ) (Set "(" (Set (Var "b")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "c")) ")" ))))) ; begin theorem :: YELLOW_5:19 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")))))) ; theorem :: YELLOW_5:20 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"Semilattice":::) (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")) ($#r3_orders_2 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r3_orders_2 :::"<="::: ) (Set (Var "c"))) & (Bool (Set (Set (Var "b")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")))))) ; theorem :: YELLOW_5:21 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")))) ")" ))) ; theorem :: YELLOW_5:22 (Bool "for" (Set (Var "L")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) (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_orders_2 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Set (Var "b")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L"))))) "holds" (Bool (Set (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")))))) ; theorem :: YELLOW_5:23 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")) ")" ) ($#k1_yellow_5 :::"\"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")))))) ; theorem :: YELLOW_5:24 (Bool "for" (Set (Var "L")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) (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")) ($#r2_yellow_5 :::"meets"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_orders_2 :::"<="::: ) (Set (Var "c")))) "holds" (Bool (Set (Var "a")) ($#r2_yellow_5 :::"meets"::: ) (Set (Var "c"))))) ; theorem :: YELLOW_5:25 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")))))) ; theorem :: YELLOW_5:26 (Bool "for" (Set (Var "L")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) (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")) ($#r2_yellow_5 :::"meets"::: ) (Set (Set (Var "b")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "c"))))) "holds" (Bool (Set (Var "a")) ($#r2_yellow_5 :::"meets"::: ) (Set (Var "b"))))) ; theorem :: YELLOW_5:27 (Bool "for" (Set (Var "L")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) (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")) ($#r2_yellow_5 :::"meets"::: ) (Set (Set (Var "b")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "c"))))) "holds" (Bool (Set (Var "a")) ($#r2_yellow_5 :::"meets"::: ) (Set (Var "b"))))) ; theorem :: YELLOW_5:28 (Bool "for" (Set (Var "L")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "a")) ($#r1_yellow_5 :::"misses"::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")))))) ; theorem :: YELLOW_5:29 (Bool "for" (Set (Var "L")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) (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_yellow_5 :::"misses"::: ) (Set (Var "c"))) & (Bool (Set (Var "b")) ($#r1_orders_2 :::"<="::: ) (Set (Var "c")))) "holds" (Bool (Set (Var "a")) ($#r1_yellow_5 :::"misses"::: ) (Set (Var "b"))))) ; theorem :: YELLOW_5:30 (Bool "for" (Set (Var "L")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool "(" (Bool (Set (Var "a")) ($#r1_yellow_5 :::"misses"::: ) (Set (Var "b"))) "or" (Bool (Set (Var "a")) ($#r1_yellow_5 :::"misses"::: ) (Set (Var "c"))) ")" )) "holds" (Bool (Set (Var "a")) ($#r1_yellow_5 :::"misses"::: ) (Set (Set (Var "b")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "c")))))) ; theorem :: YELLOW_5:31 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) (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")) ($#r3_orders_2 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r3_orders_2 :::"<="::: ) (Set (Var "c"))) & (Bool (Set (Var "b")) ($#r1_yellow_5 :::"misses"::: ) (Set (Var "c")))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")))))) ; theorem :: YELLOW_5:32 (Bool "for" (Set (Var "L")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) (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_yellow_5 :::"misses"::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "c"))) ($#r1_yellow_5 :::"misses"::: ) (Set (Set (Var "b")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "c")))))) ; begin theorem :: YELLOW_5:33 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (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 "(" (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b")) ")" ) ($#k13_lattice3 :::""\/""::: ) (Set "(" (Set (Var "b")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "c")) ")" ) ")" ) ($#k13_lattice3 :::""\/""::: ) (Set "(" (Set (Var "c")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b")) ")" ) ($#k12_lattice3 :::""/\""::: ) (Set "(" (Set (Var "b")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "c")) ")" ) ")" ) ($#k12_lattice3 :::""/\""::: ) (Set "(" (Set (Var "c")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "a")) ")" ))))) ; theorem :: YELLOW_5:34 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set "(" ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")))) & (Bool (Set (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set "(" ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow_0 :::"Top"::: ) (Set (Var "L")))) ")" ))) ; theorem :: YELLOW_5:35 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "b"))) ($#r3_orders_2 :::"<="::: ) (Set (Var "c")))) "holds" (Bool (Set (Var "a")) ($#r3_orders_2 :::"<="::: ) (Set (Set (Var "b")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "c")))))) ; theorem :: YELLOW_5:36 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k7_waybel_1 :::"'not'"::: ) (Set "(" (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "a")) ")" ) ($#k12_lattice3 :::""/\""::: ) (Set "(" ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "b")) ")" ))) & (Bool (Set ($#k7_waybel_1 :::"'not'"::: ) (Set "(" (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "a")) ")" ) ($#k13_lattice3 :::""\/""::: ) (Set "(" ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "b")) ")" ))) ")" ))) ; theorem :: YELLOW_5:37 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r3_orders_2 :::"<="::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "b"))) ($#r3_orders_2 :::"<="::: ) (Set ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "a")))))) ; theorem :: YELLOW_5:38 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (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")) ($#r3_orders_2 :::"<="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "c")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "b"))) ($#r3_orders_2 :::"<="::: ) (Set (Set (Var "c")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "a")))))) ; theorem :: YELLOW_5:39 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r3_orders_2 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r3_orders_2 :::"<="::: ) (Set (Var "d")))) "holds" (Bool (Set (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "d"))) ($#r3_orders_2 :::"<="::: ) (Set (Set (Var "b")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "c")))))) ; theorem :: YELLOW_5:40 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (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")) ($#r3_orders_2 :::"<="::: ) (Set (Set (Var "b")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "c"))))) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "b"))) ($#r3_orders_2 :::"<="::: ) (Set (Var "c"))) & (Bool (Set (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "c"))) ($#r3_orders_2 :::"<="::: ) (Set (Var "b"))) ")" ))) ; theorem :: YELLOW_5:41 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "a"))) ($#r3_orders_2 :::"<="::: ) (Set ($#k7_waybel_1 :::"'not'"::: ) (Set "(" (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b")) ")" ))) & (Bool (Set ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "b"))) ($#r3_orders_2 :::"<="::: ) (Set ($#k7_waybel_1 :::"'not'"::: ) (Set "(" (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b")) ")" ))) ")" ))) ; theorem :: YELLOW_5:42 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k7_waybel_1 :::"'not'"::: ) (Set "(" (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b")) ")" )) ($#r3_orders_2 :::"<="::: ) (Set ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "a")))) & (Bool (Set ($#k7_waybel_1 :::"'not'"::: ) (Set "(" (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b")) ")" )) ($#r3_orders_2 :::"<="::: ) (Set ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "b")))) ")" ))) ; theorem :: YELLOW_5:43 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r3_orders_2 :::"<="::: ) (Set (Set (Var "b")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "a"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")))))) ; theorem :: YELLOW_5:44 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r3_orders_2 :::"<="::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set "(" (Set (Var "b")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "a")) ")" ))))) ; theorem :: YELLOW_5:45 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")))) "iff" (Bool (Set (Var "a")) ($#r3_orders_2 :::"<="::: ) (Set (Var "b"))) ")" ))) ; theorem :: YELLOW_5:46 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (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")) ($#r3_orders_2 :::"<="::: ) (Set (Set (Var "b")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "c")))) & (Bool (Set (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L"))))) "holds" (Bool (Set (Var "a")) ($#r3_orders_2 :::"<="::: ) (Set (Var "b"))))) ; theorem :: YELLOW_5:47 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "b")) ")" ) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b")))))) ; theorem :: YELLOW_5:48 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set "(" (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")))))) ; theorem :: YELLOW_5:49 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set "(" (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "b")))))) ; theorem :: YELLOW_5:50 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "b")) ")" ) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")))))) ; theorem :: YELLOW_5:51 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set "(" (Set (Var "b")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b")))))) ; theorem :: YELLOW_5:52 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b")) ")" ) ($#k13_lattice3 :::""\/""::: ) (Set "(" (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: YELLOW_5:53 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (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_yellow_5 :::"\"::: ) (Set "(" (Set (Var "b")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "b")) ")" ) ($#k13_lattice3 :::""\/""::: ) (Set "(" (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "c")) ")" ))))) ; theorem :: YELLOW_5:54 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set "(" (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b")))))) ; theorem :: YELLOW_5:55 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b")) ")" ) ($#k1_yellow_5 :::"\"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "b")))))) ; theorem :: YELLOW_5:56 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")))) "iff" (Bool (Set (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ))) ; theorem :: YELLOW_5:57 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (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_yellow_5 :::"\"::: ) (Set "(" (Set (Var "b")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "b")) ")" ) ($#k12_lattice3 :::""/\""::: ) (Set "(" (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "c")) ")" ))))) ; theorem :: YELLOW_5:58 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (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_yellow_5 :::"\"::: ) (Set "(" (Set (Var "b")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "b")) ")" ) ($#k13_lattice3 :::""\/""::: ) (Set "(" (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "c")) ")" ))))) ; theorem :: YELLOW_5:59 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (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")) ($#k12_lattice3 :::""/\""::: ) (Set "(" (Set (Var "b")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b")) ")" ) ($#k1_yellow_5 :::"\"::: ) (Set "(" (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "c")) ")" ))))) ; theorem :: YELLOW_5:60 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b")) ")" ) ($#k1_yellow_5 :::"\"::: ) (Set "(" (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "b")) ")" ) ($#k13_lattice3 :::""\/""::: ) (Set "(" (Set (Var "b")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "a")) ")" ))))) ; theorem :: YELLOW_5:61 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (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_yellow_5 :::"\"::: ) (Set (Var "b")) ")" ) ($#k1_yellow_5 :::"\"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set "(" (Set (Var "b")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "c")) ")" ))))) ; theorem :: YELLOW_5:62 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k7_waybel_1 :::"'not'"::: ) (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow_0 :::"Top"::: ) (Set (Var "L"))))) ; theorem :: YELLOW_5:63 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k7_waybel_1 :::"'not'"::: ) (Set "(" ($#k4_yellow_0 :::"Top"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L"))))) ; theorem :: YELLOW_5:64 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")))))) ; theorem :: YELLOW_5:65 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ; theorem :: YELLOW_5:66 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k7_waybel_1 :::"'not'"::: ) (Set "(" (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "a")) ")" ) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b")))))) ; theorem :: YELLOW_5:67 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b"))) ($#r1_yellow_5 :::"misses"::: ) (Set (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "b")))))) ; theorem :: YELLOW_5:68 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k1_yellow_5 :::"\"::: ) (Set (Var "b"))) ($#r1_yellow_5 :::"misses"::: ) (Set (Var "b"))))) ; theorem :: YELLOW_5:69 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r1_yellow_5 :::"misses"::: ) (Set (Var "b")))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b")) ")" ) ($#k1_yellow_5 :::"\"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ;