:: YELLOW_7 semantic presentation begin notationlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; synonym "L" :::"opp"::: for "L" :::"~"::: ; end; theorem :: YELLOW_7:1 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) "iff" (Bool (Set ($#k9_lattice3 :::"~"::: ) (Set (Var "x"))) ($#r1_orders_2 :::">="::: ) (Set ($#k9_lattice3 :::"~"::: ) (Set (Var "y")))) ")" ))) ; theorem :: YELLOW_7:2 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ")" ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set ($#k9_lattice3 :::"~"::: ) (Set (Var "y"))))) "implies" (Bool (Set (Set (Var "x")) ($#k8_lattice3 :::"~"::: ) ) ($#r1_orders_2 :::">="::: ) (Set (Var "y"))) ")" & "(" (Bool (Bool (Set (Set (Var "x")) ($#k8_lattice3 :::"~"::: ) ) ($#r1_orders_2 :::">="::: ) (Set (Var "y")))) "implies" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set ($#k9_lattice3 :::"~"::: ) (Set (Var "y")))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r1_orders_2 :::">="::: ) (Set ($#k9_lattice3 :::"~"::: ) (Set (Var "y"))))) "implies" (Bool (Set (Set (Var "x")) ($#k8_lattice3 :::"~"::: ) ) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) ")" & "(" (Bool (Bool (Set (Set (Var "x")) ($#k8_lattice3 :::"~"::: ) ) ($#r1_orders_2 :::"<="::: ) (Set (Var "y")))) "implies" (Bool (Set (Var "x")) ($#r1_orders_2 :::">="::: ) (Set ($#k9_lattice3 :::"~"::: ) (Set (Var "y")))) ")" ")" )))) ; theorem :: YELLOW_7:3 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v2_struct_0 :::"empty"::: ) ) "iff" (Bool (Set (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ) "is" ($#v2_struct_0 :::"empty"::: ) ) ")" )) ; theorem :: YELLOW_7:4 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v3_orders_2 :::"reflexive"::: ) ) "iff" (Bool (Set (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ) "is" ($#v3_orders_2 :::"reflexive"::: ) ) ")" )) ; theorem :: YELLOW_7:5 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v5_orders_2 :::"antisymmetric"::: ) ) "iff" (Bool (Set (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ) "is" ($#v5_orders_2 :::"antisymmetric"::: ) ) ")" )) ; theorem :: YELLOW_7:6 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v4_orders_2 :::"transitive"::: ) ) "iff" (Bool (Set (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ) "is" ($#v4_orders_2 :::"transitive"::: ) ) ")" )) ; theorem :: YELLOW_7:7 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v16_waybel_0 :::"connected"::: ) ) "iff" (Bool (Set (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ) "is" ($#v16_waybel_0 :::"connected"::: ) ) ")" )) ; registrationlet "L" be ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "L" ($#k7_lattice3 :::"opp"::: ) ) -> ($#v3_orders_2 :::"reflexive"::: ) ; end; registrationlet "L" be ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "L" ($#k7_lattice3 :::"opp"::: ) ) -> ($#v4_orders_2 :::"transitive"::: ) ; end; registrationlet "L" be ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "L" ($#k7_lattice3 :::"opp"::: ) ) -> ($#v5_orders_2 :::"antisymmetric"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "L" ($#k7_lattice3 :::"opp"::: ) ) -> ($#v16_waybel_0 :::"connected"::: ) ; end; theorem :: YELLOW_7:8 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X")))) "implies" (Bool (Set (Set (Var "x")) ($#k8_lattice3 :::"~"::: ) ) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X"))) ")" & "(" (Bool (Bool (Set (Set (Var "x")) ($#k8_lattice3 :::"~"::: ) ) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X")))) "implies" (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X"))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X")))) "implies" (Bool (Set (Set (Var "x")) ($#k8_lattice3 :::"~"::: ) ) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X"))) ")" & "(" (Bool (Bool (Set (Set (Var "x")) ($#k8_lattice3 :::"~"::: ) ) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X")))) "implies" (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X"))) ")" ")" )))) ; theorem :: YELLOW_7:9 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ")" ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X")))) "implies" (Bool (Set ($#k9_lattice3 :::"~"::: ) (Set (Var "x"))) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X"))) ")" & "(" (Bool (Bool (Set ($#k9_lattice3 :::"~"::: ) (Set (Var "x"))) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X")))) "implies" (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X"))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X")))) "implies" (Bool (Set ($#k9_lattice3 :::"~"::: ) (Set (Var "x"))) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X"))) ")" & "(" (Bool (Bool (Set ($#k9_lattice3 :::"~"::: ) (Set (Var "x"))) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X")))) "implies" (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X"))) ")" ")" )))) ; theorem :: YELLOW_7:10 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) "iff" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) )) ")" ))) ; theorem :: YELLOW_7:11 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) )) "iff" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) ")" ))) ; theorem :: YELLOW_7:12 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) "or" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) )) ")" )) "holds" (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set "(" (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ")" ) ")" )))) ; theorem :: YELLOW_7:13 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) "or" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) )) ")" )) "holds" (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set "(" (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ")" ) ")" )))) ; theorem :: YELLOW_7:14 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L2"))) "#)" )) & (Bool (Set (Var "L1")) "is" ($#v2_lattice3 :::"with_infima"::: ) )) "holds" (Bool (Set (Var "L2")) "is" ($#v2_lattice3 :::"with_infima"::: ) )) ; theorem :: YELLOW_7:15 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L2"))) "#)" )) & (Bool (Set (Var "L1")) "is" ($#v1_lattice3 :::"with_suprema"::: ) )) "holds" (Bool (Set (Var "L2")) "is" ($#v1_lattice3 :::"with_suprema"::: ) )) ; theorem :: YELLOW_7:16 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v2_lattice3 :::"with_infima"::: ) ) "iff" (Bool (Set (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ) "is" ($#v1_lattice3 :::"with_suprema"::: ) ) ")" )) ; theorem :: YELLOW_7:17 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v3_lattice3 :::"complete"::: ) ) "iff" (Bool (Set (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ) "is" ($#v3_lattice3 :::"complete"::: ) ) ")" )) ; registrationlet "L" be ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "L" ($#k7_lattice3 :::"opp"::: ) ) -> ($#v1_lattice3 :::"with_suprema"::: ) ; end; registrationlet "L" be ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "L" ($#k7_lattice3 :::"opp"::: ) ) -> ($#v2_lattice3 :::"with_infima"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "L" ($#k7_lattice3 :::"opp"::: ) ) -> ($#v3_lattice3 :::"complete"::: ) ; end; theorem :: YELLOW_7:18 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ")" ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y")))) "holds" (Bool "(" (Bool (Set ($#k12_waybel_0 :::"fininfs"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k11_waybel_0 :::"finsups"::: ) (Set (Var "Y")))) & (Bool (Set ($#k11_waybel_0 :::"finsups"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k12_waybel_0 :::"fininfs"::: ) (Set (Var "Y")))) ")" )))) ; theorem :: YELLOW_7:19 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ")" ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y")))) "holds" (Bool "(" (Bool (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "Y")))) & (Bool (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "Y")))) ")" )))) ; theorem :: YELLOW_7:20 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool "(" (Bool (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "y")))) & (Bool (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "y")))) ")" )))) ; theorem :: YELLOW_7:21 (Bool "for" (Set (Var "L")) "being" ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "x")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k8_lattice3 :::"~"::: ) ")" ) ($#k13_lattice3 :::""\/""::: ) (Set "(" (Set (Var "y")) ($#k8_lattice3 :::"~"::: ) ")" ))))) ; theorem :: YELLOW_7:22 (Bool "for" (Set (Var "L")) "being" ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ")" ) "holds" (Bool (Set (Set "(" ($#k9_lattice3 :::"~"::: ) (Set (Var "x")) ")" ) ($#k12_lattice3 :::""/\""::: ) (Set "(" ($#k9_lattice3 :::"~"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "y")))))) ; theorem :: YELLOW_7:23 (Bool "for" (Set (Var "L")) "being" ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "x")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k8_lattice3 :::"~"::: ) ")" ) ($#k12_lattice3 :::""/\""::: ) (Set "(" (Set (Var "y")) ($#k8_lattice3 :::"~"::: ) ")" ))))) ; theorem :: YELLOW_7:24 (Bool "for" (Set (Var "L")) "being" ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ")" ) "holds" (Bool (Set (Set "(" ($#k9_lattice3 :::"~"::: ) (Set (Var "x")) ")" ) ($#k13_lattice3 :::""\/""::: ) (Set "(" ($#k9_lattice3 :::"~"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "y")))))) ; theorem :: YELLOW_7:25 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v2_waybel_1 :::"distributive"::: ) ) "iff" (Bool (Set (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ) "is" ($#v2_waybel_1 :::"distributive"::: ) ) ")" )) ; registrationlet "L" be ($#v2_waybel_1 :::"distributive"::: ) ($#l1_orders_2 :::"LATTICE":::); cluster (Set "L" ($#k7_lattice3 :::"opp"::: ) ) -> ($#v2_waybel_1 :::"distributive"::: ) ; end; theorem :: YELLOW_7:26 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L"))) "iff" (Bool (Set (Var "x")) "is" ($#v2_waybel_0 :::"filtered"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ")" )) ")" ))) ; theorem :: YELLOW_7:27 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ")" )) "iff" (Bool (Set (Var "x")) "is" ($#v2_waybel_0 :::"filtered"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L"))) ")" ))) ; theorem :: YELLOW_7:28 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v12_waybel_0 :::"lower"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L"))) "iff" (Bool (Set (Var "x")) "is" ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ")" )) ")" ))) ; theorem :: YELLOW_7:29 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v12_waybel_0 :::"lower"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ")" )) "iff" (Bool (Set (Var "x")) "is" ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L"))) ")" ))) ; theorem :: YELLOW_7:30 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_yellow_0 :::"lower-bounded"::: ) ) "iff" (Bool (Set (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ) "is" ($#v2_yellow_0 :::"upper-bounded"::: ) ) ")" )) ; theorem :: YELLOW_7:31 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ) "is" ($#v1_yellow_0 :::"lower-bounded"::: ) ) "iff" (Bool (Set (Var "L")) "is" ($#v2_yellow_0 :::"upper-bounded"::: ) ) ")" )) ; theorem :: YELLOW_7:32 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v3_yellow_0 :::"bounded"::: ) ) "iff" (Bool (Set (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ) "is" ($#v3_yellow_0 :::"bounded"::: ) ) ")" )) ; theorem :: YELLOW_7:33 (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"::: ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")) ")" ) ($#k8_lattice3 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow_0 :::"Top"::: ) (Set "(" (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ")" ))) & (Bool (Set ($#k9_lattice3 :::"~"::: ) (Set "(" ($#k4_yellow_0 :::"Top"::: ) (Set "(" (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")))) ")" )) ; theorem :: YELLOW_7:34 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_yellow_0 :::"Top"::: ) (Set (Var "L")) ")" ) ($#k8_lattice3 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set "(" (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ")" ))) & (Bool (Set ($#k9_lattice3 :::"~"::: ) (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) (Set "(" (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow_0 :::"Top"::: ) (Set (Var "L")))) ")" )) ; theorem :: YELLOW_7:35 (Bool "for" (Set (Var "L")) "being" ($#v3_yellow_0 :::"bounded"::: ) ($#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 (Set (Var "y")) ($#k8_lattice3 :::"~"::: ) ) ($#r6_waybel_1 :::"is_a_complement_of"::: ) (Set (Set (Var "x")) ($#k8_lattice3 :::"~"::: ) )) ")" ))) ; theorem :: YELLOW_7:36 (Bool "for" (Set (Var "L")) "being" ($#v3_yellow_0 :::"bounded"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v10_waybel_1 :::"complemented"::: ) ) "iff" (Bool (Set (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ) "is" ($#v10_waybel_1 :::"complemented"::: ) ) ")" )) ; registrationlet "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "L" ($#k7_lattice3 :::"opp"::: ) ) -> ($#v2_yellow_0 :::"upper-bounded"::: ) ; end; registrationlet "L" be ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "L" ($#k7_lattice3 :::"opp"::: ) ) -> ($#v1_yellow_0 :::"lower-bounded"::: ) ; end; registrationlet "L" be ($#v3_yellow_0 :::"bounded"::: ) ($#v10_waybel_1 :::"complemented"::: ) ($#l1_orders_2 :::"LATTICE":::); cluster (Set "L" ($#k7_lattice3 :::"opp"::: ) ) -> ($#v10_waybel_1 :::"complemented"::: ) ; end; theorem :: YELLOW_7:37 (Bool "for" (Set (Var "L")) "being" ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k7_waybel_1 :::"'not'"::: ) (Set "(" (Set (Var "x")) ($#k8_lattice3 :::"~"::: ) ")" )) ($#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"::: ) ; func :::"ComplMap"::: "L" -> ($#m1_subset_1 :::"Function":::) "of" "L" "," (Set "(" "L" ($#k7_lattice3 :::"opp"::: ) ")" ) means :: YELLOW_7:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "x"))))); end; :: deftheorem defines :::"ComplMap"::: YELLOW_7:def 1 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set "(" (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_7 :::"ComplMap"::: ) (Set (Var "L")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k7_waybel_1 :::"'not'"::: ) (Set (Var "x"))))) ")" ))); registrationlet "L" be ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"LATTICE":::); cluster (Set ($#k1_yellow_7 :::"ComplMap"::: ) "L") -> bbbadV2_FUNCT_1() ; end; registrationlet "L" be ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"LATTICE":::); cluster (Set ($#k1_yellow_7 :::"ComplMap"::: ) "L") -> ($#v23_waybel_0 :::"isomorphic"::: ) ; end; theorem :: YELLOW_7:38 (Bool "for" (Set (Var "L")) "being" ($#v11_waybel_1 :::"Boolean"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool (Set (Var "L")) "," (Set (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ) ($#r5_waybel_1 :::"are_isomorphic"::: ) )) ; theorem :: YELLOW_7:39 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")))) "implies" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "S")) ($#k7_lattice3 :::"opp"::: ) ")" ) "," (Set (Var "T"))) ")" & "(" (Bool (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "S")) ($#k7_lattice3 :::"opp"::: ) ")" ) "," (Set (Var "T")))) "implies" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))) ")" & "(" (Bool (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")))) "implies" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set "(" (Set (Var "T")) ($#k7_lattice3 :::"opp"::: ) ")" )) ")" & "(" (Bool (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set "(" (Set (Var "T")) ($#k7_lattice3 :::"opp"::: ) ")" ))) "implies" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))) ")" & "(" (Bool (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")))) "implies" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "S")) ($#k7_lattice3 :::"opp"::: ) ")" ) "," (Set "(" (Set (Var "T")) ($#k7_lattice3 :::"opp"::: ) ")" )) ")" & "(" (Bool (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "S")) ($#k7_lattice3 :::"opp"::: ) ")" ) "," (Set "(" (Set (Var "T")) ($#k7_lattice3 :::"opp"::: ) ")" ))) "implies" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))) ")" ")" ))) ; theorem :: YELLOW_7:40 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set "(" (Set (Var "T")) ($#k7_lattice3 :::"opp"::: ) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) )) "implies" (Bool (Set (Var "g")) "is" ($#v5_waybel_0 :::"antitone"::: ) ) ")" & "(" (Bool (Bool (Set (Var "g")) "is" ($#v5_waybel_0 :::"antitone"::: ) )) "implies" (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) ) ")" & "(" (Bool (Bool (Set (Var "f")) "is" ($#v5_waybel_0 :::"antitone"::: ) )) "implies" (Bool (Set (Var "g")) "is" ($#v5_orders_3 :::"monotone"::: ) ) ")" & "(" (Bool (Bool (Set (Var "g")) "is" ($#v5_orders_3 :::"monotone"::: ) )) "implies" (Bool (Set (Var "f")) "is" ($#v5_waybel_0 :::"antitone"::: ) ) ")" ")" )))) ; theorem :: YELLOW_7:41 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set "(" (Set (Var "T")) ($#k7_lattice3 :::"opp"::: ) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "S")) ($#k7_lattice3 :::"opp"::: ) ")" ) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) )) "implies" (Bool (Set (Var "g")) "is" ($#v5_orders_3 :::"monotone"::: ) ) ")" & "(" (Bool (Bool (Set (Var "g")) "is" ($#v5_orders_3 :::"monotone"::: ) )) "implies" (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) ) ")" & "(" (Bool (Bool (Set (Var "f")) "is" ($#v5_waybel_0 :::"antitone"::: ) )) "implies" (Bool (Set (Var "g")) "is" ($#v5_waybel_0 :::"antitone"::: ) ) ")" & "(" (Bool (Bool (Set (Var "g")) "is" ($#v5_waybel_0 :::"antitone"::: ) )) "implies" (Bool (Set (Var "f")) "is" ($#v5_waybel_0 :::"antitone"::: ) ) ")" ")" )))) ; theorem :: YELLOW_7:42 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "S")) ($#k7_lattice3 :::"opp"::: ) ")" ) "," (Set "(" (Set (Var "T")) ($#k7_lattice3 :::"opp"::: ) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) )) "implies" (Bool (Set (Var "g")) "is" ($#v5_orders_3 :::"monotone"::: ) ) ")" & "(" (Bool (Bool (Set (Var "g")) "is" ($#v5_orders_3 :::"monotone"::: ) )) "implies" (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) ) ")" & "(" (Bool (Bool (Set (Var "f")) "is" ($#v5_waybel_0 :::"antitone"::: ) )) "implies" (Bool (Set (Var "g")) "is" ($#v5_waybel_0 :::"antitone"::: ) ) ")" & "(" (Bool (Bool (Set (Var "g")) "is" ($#v5_waybel_0 :::"antitone"::: ) )) "implies" (Bool (Set (Var "f")) "is" ($#v5_waybel_0 :::"antitone"::: ) ) ")" ")" )))) ; theorem :: YELLOW_7:43 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "f")) "is" ($#m1_waybel_1 :::"Connection"::: ) "of" (Set (Var "S")) "," (Set (Var "T")))) "implies" (Bool (Set (Var "f")) "is" ($#m1_waybel_1 :::"Connection"::: ) "of" (Set (Set (Var "S")) ($#k7_lattice3 :::"~"::: ) ) "," (Set (Var "T"))) ")" & "(" (Bool (Bool (Set (Var "f")) "is" ($#m1_waybel_1 :::"Connection"::: ) "of" (Set (Set (Var "S")) ($#k7_lattice3 :::"~"::: ) ) "," (Set (Var "T")))) "implies" (Bool (Set (Var "f")) "is" ($#m1_waybel_1 :::"Connection"::: ) "of" (Set (Var "S")) "," (Set (Var "T"))) ")" & "(" (Bool (Bool (Set (Var "f")) "is" ($#m1_waybel_1 :::"Connection"::: ) "of" (Set (Var "S")) "," (Set (Var "T")))) "implies" (Bool (Set (Var "f")) "is" ($#m1_waybel_1 :::"Connection"::: ) "of" (Set (Var "S")) "," (Set (Set (Var "T")) ($#k7_lattice3 :::"~"::: ) )) ")" & "(" (Bool (Bool (Set (Var "f")) "is" ($#m1_waybel_1 :::"Connection"::: ) "of" (Set (Var "S")) "," (Set (Set (Var "T")) ($#k7_lattice3 :::"~"::: ) ))) "implies" (Bool (Set (Var "f")) "is" ($#m1_waybel_1 :::"Connection"::: ) "of" (Set (Var "S")) "," (Set (Var "T"))) ")" & "(" (Bool (Bool (Set (Var "f")) "is" ($#m1_waybel_1 :::"Connection"::: ) "of" (Set (Var "S")) "," (Set (Var "T")))) "implies" (Bool (Set (Var "f")) "is" ($#m1_waybel_1 :::"Connection"::: ) "of" (Set (Set (Var "S")) ($#k7_lattice3 :::"~"::: ) ) "," (Set (Set (Var "T")) ($#k7_lattice3 :::"~"::: ) )) ")" & "(" (Bool (Bool (Set (Var "f")) "is" ($#m1_waybel_1 :::"Connection"::: ) "of" (Set (Set (Var "S")) ($#k7_lattice3 :::"~"::: ) ) "," (Set (Set (Var "T")) ($#k7_lattice3 :::"~"::: ) ))) "implies" (Bool (Set (Var "f")) "is" ($#m1_waybel_1 :::"Connection"::: ) "of" (Set (Var "S")) "," (Set (Var "T"))) ")" ")" ))) ; theorem :: YELLOW_7:44 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "g1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "S")) ($#k7_lattice3 :::"~"::: ) ")" ) "," (Set "(" (Set (Var "T")) ($#k7_lattice3 :::"~"::: ) ")" ) (Bool "for" (Set (Var "g2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "T")) ($#k7_lattice3 :::"~"::: ) ")" ) "," (Set "(" (Set (Var "S")) ($#k7_lattice3 :::"~"::: ) ")" ) "st" (Bool (Bool (Set (Var "f1")) ($#r1_funct_2 :::"="::: ) (Set (Var "f2"))) & (Bool (Set (Var "g1")) ($#r1_funct_2 :::"="::: ) (Set (Var "g2")))) "holds" (Bool "(" (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set (Var "f1")) "," (Set (Var "g1")) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) ) "iff" (Bool (Set ($#k1_waybel_1 :::"["::: ) (Set (Var "g2")) "," (Set (Var "f2")) ($#k1_waybel_1 :::"]"::: ) ) "is" ($#v3_waybel_1 :::"Galois"::: ) ) ")" )))))) ; theorem :: YELLOW_7:45 (Bool "for" (Set (Var "J")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "K")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "J")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Var "K")) "," (Set (Var "D")) "holds" (Bool (Set ($#k2_funct_6 :::"doms"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "K"))))))) ; definitionlet "J", "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "K" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "J")); let "F" be ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Const "K")) "," (Set (Const "D")); let "j" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "J")); let "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Const "K")) ($#k1_funct_1 :::"."::: ) (Set (Const "j"))); :: original: :::".."::: redefine func "F" :::".."::: "(" "j" "," "k" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" "D"; end; theorem :: YELLOW_7:46 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "K")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "J")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Var "K")) "," (Set (Var "L"))) "iff" (Bool (Set (Var "x")) "is" ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Var "K")) "," (Set "(" (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ")" )) ")" ))))) ; theorem :: YELLOW_7:47 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "J")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "K")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "J")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Var "K")) "," (Set (Var "L")) "holds" (Bool (Set ($#k4_yellow_2 :::"Sup"::: ) ) ($#r3_orders_2 :::"<="::: ) (Set ($#k5_yellow_2 :::"Inf"::: ) )))))) ; theorem :: YELLOW_7:48 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_waybel_5 :::"completely-distributive"::: ) ) "iff" (Bool "for" (Set (Var "J")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "K")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "J")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"DoubleIndexedSet":::) "of" (Set (Var "K")) "," (Set (Var "L")) "holds" (Bool (Set ($#k4_yellow_2 :::"Sup"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_yellow_2 :::"Inf"::: ) ))))) ")" )) ; theorem :: YELLOW_7:49 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k4_yellow_2 :::"\\/"::: ) "(" (Set (Var "F")) "," (Set (Var "L")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_yellow_2 :::"//\"::: ) "(" (Set (Var "F")) "," (Set "(" (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ")" ) ")" )) & (Bool (Set ($#k5_yellow_2 :::"//\"::: ) "(" (Set (Var "F")) "," (Set (Var "L")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow_2 :::"\\/"::: ) "(" (Set (Var "F")) "," (Set "(" (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ")" ) ")" )) ")" ))) ; theorem :: YELLOW_7:50 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k4_waybel_5 :::"\//"::: ) "(" (Set (Var "F")) "," (Set (Var "L")) ")" ) ($#r1_funct_2 :::"="::: ) (Set ($#k5_waybel_5 :::"/\\"::: ) "(" (Set (Var "F")) "," (Set "(" (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ")" ) ")" )) & (Bool (Set ($#k5_waybel_5 :::"/\\"::: ) "(" (Set (Var "F")) "," (Set (Var "L")) ")" ) ($#r1_funct_2 :::"="::: ) (Set ($#k4_waybel_5 :::"\//"::: ) "(" (Set (Var "F")) "," (Set "(" (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ")" ) ")" )) ")" ))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_waybel_5 :::"completely-distributive"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) bbbadV7_STRUCT_0() ($#v8_struct_0 :::"finite"::: ) (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v1_orders_2 :::"strict"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v3_lattice3 :::"complete"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v2_yellow_0 :::"upper-bounded"::: ) ($#v3_yellow_0 :::"bounded"::: ) ($#v16_waybel_0 :::"connected"::: ) ($#v24_waybel_0 :::"up-complete"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) ($#v2_waybel_1 :::"distributive"::: ) bbbadV9_WAYBEL_1() ($#v1_waybel_5 :::"completely-distributive"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; theorem :: YELLOW_7:51 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_waybel_5 :::"completely-distributive"::: ) ) "iff" (Bool (Set (Set (Var "L")) ($#k7_lattice3 :::"opp"::: ) ) "is" ($#v1_waybel_5 :::"completely-distributive"::: ) ) ")" )) ;