:: YELLOW_4 semantic presentation begin theorem :: YELLOW_4:1 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) "holds" (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ))))) ; theorem :: YELLOW_4:2 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) "holds" (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) ($#r1_orders_2 :::"<="::: ) (Set (Var "a")))))) ; definitionlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; let "A", "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); pred "A" :::"is_finer_than"::: "B" means :: YELLOW_4:def 1 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "A")) "holds" (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) "B") & (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b"))) ")" ))); pred "B" :::"is_coarser_than"::: "A" means :: YELLOW_4:def 2 (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) "B")) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b"))) ")" ))); end; :: deftheorem defines :::"is_finer_than"::: YELLOW_4:def 1 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_yellow_4 :::"is_finer_than"::: ) (Set (Var "B"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b"))) ")" ))) ")" ))); :: deftheorem defines :::"is_coarser_than"::: YELLOW_4:def 2 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "B")) ($#r2_yellow_4 :::"is_coarser_than"::: ) (Set (Var "A"))) "iff" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b"))) ")" ))) ")" ))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "A", "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); :: original: :::"is_finer_than"::: redefine pred "A" :::"is_finer_than"::: "B"; reflexivity (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")) "holds" (Bool ((Set (Const "L")) "," (Set (Var "b1")) "," (Set (Var "b1"))))) ; :: original: :::"is_coarser_than"::: redefine pred "B" :::"is_coarser_than"::: "A"; reflexivity (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")) "holds" (Bool ((Set (Const "L")) "," (Set (Var "b1")) "," (Set (Var "b1"))))) ; end; theorem :: YELLOW_4:3 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "L"))) ($#r1_yellow_4 :::"is_finer_than"::: ) (Set (Var "B"))))) ; theorem :: YELLOW_4:4 (Bool "for" (Set (Var "L")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "A")) ($#r1_yellow_4 :::"is_finer_than"::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) ($#r1_yellow_4 :::"is_finer_than"::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "A")) ($#r1_yellow_4 :::"is_finer_than"::: ) (Set (Var "C"))))) ; theorem :: YELLOW_4:5 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "B")) ($#r1_yellow_4 :::"is_finer_than"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) "is" ($#v12_waybel_0 :::"lower"::: ) )) "holds" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))))) ; theorem :: YELLOW_4:6 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "L"))) ($#r2_yellow_4 :::"is_coarser_than"::: ) (Set (Var "A"))))) ; theorem :: YELLOW_4:7 (Bool "for" (Set (Var "L")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "C")) ($#r2_yellow_4 :::"is_coarser_than"::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) ($#r2_yellow_4 :::"is_coarser_than"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "C")) ($#r2_yellow_4 :::"is_coarser_than"::: ) (Set (Var "A"))))) ; theorem :: YELLOW_4:8 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "A")) ($#r2_yellow_4 :::"is_coarser_than"::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) "is" ($#v13_waybel_0 :::"upper"::: ) )) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))))) ; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "D1", "D2" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); func "D1" :::""\/""::: "D2" -> ($#m1_subset_1 :::"Subset":::) "of" "L" equals :: YELLOW_4:def 3 "{" (Set "(" (Set (Var "x")) ($#k10_lattice3 :::""\/""::: ) (Set (Var "y")) ")" ) where x, y "is" ($#m1_subset_1 :::"Element":::) "of" "L" : (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "D1") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "D2") ")" ) "}" ; end; :: deftheorem defines :::""\/""::: YELLOW_4:def 3 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "D1")) ($#k1_yellow_4 :::""\/""::: ) (Set (Var "D2"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "x")) ($#k10_lattice3 :::""\/""::: ) (Set (Var "y")) ")" ) where x, y "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "D1"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "D2"))) ")" ) "}" ))); definitionlet "L" be ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "D1", "D2" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); :: original: :::""\/""::: redefine func "D1" :::""\/""::: "D2" -> ($#m1_subset_1 :::"Subset":::) "of" "L"; commutativity (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")) "holds" (Bool (Set (Set (Var "D1")) ($#k1_yellow_4 :::""\/""::: ) (Set (Var "D2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "D2")) ($#k1_yellow_4 :::""\/""::: ) (Set (Var "D1"))))) ; end; theorem :: YELLOW_4:9 (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")) "holds" (Bool (Set (Set (Var "X")) ($#k1_yellow_4 :::""\/""::: ) (Set "(" ($#k1_struct_0 :::"{}"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: YELLOW_4:10 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "x")) ($#k10_lattice3 :::""\/""::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k1_yellow_4 :::""\/""::: ) (Set (Var "Y"))))))) ; theorem :: YELLOW_4:11 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "A")) ($#r1_yellow_4 :::"is_finer_than"::: ) (Set (Set (Var "A")) ($#k2_yellow_4 :::""\/""::: ) (Set (Var "B"))))))) ; theorem :: YELLOW_4:12 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "A")) ($#k2_yellow_4 :::""\/""::: ) (Set (Var "B"))) ($#r2_yellow_4 :::"is_coarser_than"::: ) (Set (Var "A"))))) ; theorem :: YELLOW_4:13 (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 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k2_yellow_4 :::""\/""::: ) (Set (Var "A")))))) ; theorem :: YELLOW_4:14 (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 "D1")) "," (Set (Var "D2")) "," (Set (Var "D3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "D1")) ($#k2_yellow_4 :::""\/""::: ) (Set (Var "D2")) ")" ) ($#k2_yellow_4 :::""\/""::: ) (Set (Var "D3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "D1")) ($#k2_yellow_4 :::""\/""::: ) (Set "(" (Set (Var "D2")) ($#k2_yellow_4 :::""\/""::: ) (Set (Var "D3")) ")" ))))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "D1", "D2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set "D1" ($#k1_yellow_4 :::""\/""::: ) "D2") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "L" be ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "D1", "D2" be ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set "D1" ($#k1_yellow_4 :::""\/""::: ) "D2") -> ($#v1_waybel_0 :::"directed"::: ) ; end; registrationlet "L" be ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "D1", "D2" be ($#v2_waybel_0 :::"filtered"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set "D1" ($#k1_yellow_4 :::""\/""::: ) "D2") -> ($#v2_waybel_0 :::"filtered"::: ) ; end; registrationlet "L" be ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"Poset":::); let "D1", "D2" be ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set "D1" ($#k1_yellow_4 :::""\/""::: ) "D2") -> ($#v13_waybel_0 :::"upper"::: ) ; end; theorem :: YELLOW_4:15 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k1_yellow_4 :::""\/""::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "x")) ($#k10_lattice3 :::""\/""::: ) (Set (Var "y")) ")" ) where y "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) "}" )))) ; theorem :: YELLOW_4:16 (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")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "A")) ($#k1_yellow_4 :::""\/""::: ) (Set "(" (Set (Var "B")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k1_yellow_4 :::""\/""::: ) (Set (Var "B")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "A")) ($#k1_yellow_4 :::""\/""::: ) (Set (Var "C")) ")" ))))) ; theorem :: YELLOW_4:17 (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")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "B")) ($#k2_yellow_4 :::""\/""::: ) (Set (Var "C")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ) ($#k2_yellow_4 :::""\/""::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")) ")" ))))) ; theorem :: YELLOW_4:18 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ) ($#k2_yellow_4 :::""\/""::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "B")) ($#k2_yellow_4 :::""\/""::: ) (Set (Var "C")) ")" )))))) ; theorem :: YELLOW_4:19 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k1_yellow_4 :::""\/""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "x")) ($#k10_lattice3 :::""\/""::: ) (Set (Var "y")) ")" ) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: YELLOW_4:20 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k1_yellow_4 :::""\/""::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k7_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set "(" (Set (Var "x")) ($#k10_lattice3 :::""\/""::: ) (Set (Var "y")) ")" ) "," (Set "(" (Set (Var "x")) ($#k10_lattice3 :::""\/""::: ) (Set (Var "z")) ")" ) ($#k7_domain_1 :::"}"::: ) )))) ; theorem :: YELLOW_4:21 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tarski :::"c="::: ) (Set (Var "Y1"))) & (Bool (Set (Var "X2")) ($#r1_tarski :::"c="::: ) (Set (Var "Y2")))) "holds" (Bool (Set (Set (Var "X1")) ($#k1_yellow_4 :::""\/""::: ) (Set (Var "X2"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "Y1")) ($#k1_yellow_4 :::""\/""::: ) (Set (Var "Y2")))))) ; theorem :: YELLOW_4:22 (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 "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k2_yellow_4 :::""\/""::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set (Var "D")))))) ; theorem :: YELLOW_4:23 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k2_yellow_4 :::""\/""::: ) (Set (Var "D"))))))) ; theorem :: YELLOW_4:24 (Bool "for" (Set (Var "L")) "being" ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k2_yellow_4 :::""\/""::: ) (Set (Var "X"))) "," (Set (Var "L"))) & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) "holds" (Bool (Set (Set (Var "x")) ($#k13_lattice3 :::""\/""::: ) (Set "(" ($#k2_yellow_0 :::"inf"::: ) (Set (Var "X")) ")" )) ($#r3_orders_2 :::"<="::: ) (Set ($#k2_yellow_0 :::"inf"::: ) (Set "(" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k2_yellow_4 :::""\/""::: ) (Set (Var "X")) ")" )))))) ; theorem :: YELLOW_4:25 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "A")) ($#r2_lattice3 :::"is_<=_than"::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" (Set (Var "A")) ($#k2_yellow_4 :::""\/""::: ) (Set (Var "B")) ")" )))))) ; theorem :: YELLOW_4:26 (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")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b"))) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Set (Var "A")) ($#k2_yellow_4 :::""\/""::: ) (Set (Var "B"))))))) ; theorem :: YELLOW_4:27 (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")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b"))) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Set (Var "A")) ($#k2_yellow_4 :::""\/""::: ) (Set (Var "B"))))))) ; theorem :: YELLOW_4:28 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" (Set (Var "A")) ($#k2_yellow_4 :::""\/""::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_yellow_0 :::"sup"::: ) (Set (Var "A")) ")" ) ($#k13_lattice3 :::""\/""::: ) (Set "(" ($#k1_yellow_0 :::"sup"::: ) (Set (Var "B")) ")" ))))) ; theorem :: YELLOW_4:29 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set "(" (Set (Var "X")) ($#k2_yellow_4 :::""\/""::: ) (Set (Var "Y")) ")" )))))) ; theorem :: YELLOW_4:30 (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 "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set (Var "L")) ")" ) ")" ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "x")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set "(" (Set (Var "X")) ($#k2_yellow_4 :::""\/""::: ) (Set (Var "Y")) ")" )))))) ; theorem :: YELLOW_4:31 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "L")) "," (Set (Var "L")) ($#k3_yellow_3 :::":]"::: ) ) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) "{" (Set (Var "X")) where X "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) : (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k1_yellow_4 :::""\/""::: ) (Set "(" ($#k5_yellow_3 :::"proj2"::: ) (Set (Var "D")) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_yellow_3 :::"proj1"::: ) (Set (Var "D")))) ")" )) "}" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_yellow_3 :::"proj1"::: ) (Set (Var "D")) ")" ) ($#k1_yellow_4 :::""\/""::: ) (Set "(" ($#k5_yellow_3 :::"proj2"::: ) (Set (Var "D")) ")" ))))) ; theorem :: YELLOW_4:32 (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 "D1")) "," (Set (Var "D2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set "(" (Set "(" ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "D1")) ")" ) ($#k2_yellow_4 :::""\/""::: ) (Set "(" ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "D2")) ")" ) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set "(" (Set (Var "D1")) ($#k2_yellow_4 :::""\/""::: ) (Set (Var "D2")) ")" ))))) ; theorem :: YELLOW_4:33 (Bool "for" (Set (Var "L")) "being" ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set "(" (Set "(" ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "D1")) ")" ) ($#k2_yellow_4 :::""\/""::: ) (Set "(" ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "D2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set "(" (Set (Var "D1")) ($#k2_yellow_4 :::""\/""::: ) (Set (Var "D2")) ")" ))))) ; theorem :: YELLOW_4:34 (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 "D1")) "," (Set (Var "D2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set "(" (Set "(" ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "D1")) ")" ) ($#k2_yellow_4 :::""\/""::: ) (Set "(" ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "D2")) ")" ) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set "(" (Set (Var "D1")) ($#k2_yellow_4 :::""\/""::: ) (Set (Var "D2")) ")" ))))) ; theorem :: YELLOW_4:35 (Bool "for" (Set (Var "L")) "being" ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set "(" (Set "(" ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "D1")) ")" ) ($#k2_yellow_4 :::""\/""::: ) (Set "(" ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "D2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set "(" (Set (Var "D1")) ($#k2_yellow_4 :::""\/""::: ) (Set (Var "D2")) ")" ))))) ; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "D1", "D2" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); func "D1" :::""/\""::: "D2" -> ($#m1_subset_1 :::"Subset":::) "of" "L" equals :: YELLOW_4:def 4 "{" (Set "(" (Set (Var "x")) ($#k11_lattice3 :::""/\""::: ) (Set (Var "y")) ")" ) where x, y "is" ($#m1_subset_1 :::"Element":::) "of" "L" : (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "D1") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "D2") ")" ) "}" ; end; :: deftheorem defines :::""/\""::: YELLOW_4:def 4 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "D1")) ($#k3_yellow_4 :::""/\""::: ) (Set (Var "D2"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "x")) ($#k11_lattice3 :::""/\""::: ) (Set (Var "y")) ")" ) where x, y "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "D1"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "D2"))) ")" ) "}" ))); definitionlet "L" be ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "D1", "D2" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); :: original: :::""/\""::: redefine func "D1" :::""/\""::: "D2" -> ($#m1_subset_1 :::"Subset":::) "of" "L"; commutativity (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")) "holds" (Bool (Set (Set (Var "D1")) ($#k3_yellow_4 :::""/\""::: ) (Set (Var "D2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "D2")) ($#k3_yellow_4 :::""/\""::: ) (Set (Var "D1"))))) ; end; theorem :: YELLOW_4:36 (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")) "holds" (Bool (Set (Set (Var "X")) ($#k3_yellow_4 :::""/\""::: ) (Set "(" ($#k1_struct_0 :::"{}"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: YELLOW_4:37 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "x")) ($#k11_lattice3 :::""/\""::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k3_yellow_4 :::""/\""::: ) (Set (Var "Y"))))))) ; theorem :: YELLOW_4:38 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "A")) ($#r2_yellow_4 :::"is_coarser_than"::: ) (Set (Set (Var "A")) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "B"))))))) ; theorem :: YELLOW_4:39 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "A")) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "B"))) ($#r1_yellow_4 :::"is_finer_than"::: ) (Set (Var "A"))))) ; theorem :: YELLOW_4:40 (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 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "A")))))) ; theorem :: YELLOW_4:41 (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 "D1")) "," (Set (Var "D2")) "," (Set (Var "D3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "D1")) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "D2")) ")" ) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "D3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "D1")) ($#k4_yellow_4 :::""/\""::: ) (Set "(" (Set (Var "D2")) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "D3")) ")" ))))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "D1", "D2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set "D1" ($#k3_yellow_4 :::""/\""::: ) "D2") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "L" be ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "D1", "D2" be ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set "D1" ($#k3_yellow_4 :::""/\""::: ) "D2") -> ($#v1_waybel_0 :::"directed"::: ) ; end; registrationlet "L" be ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "D1", "D2" be ($#v2_waybel_0 :::"filtered"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set "D1" ($#k3_yellow_4 :::""/\""::: ) "D2") -> ($#v2_waybel_0 :::"filtered"::: ) ; end; registrationlet "L" be ($#l1_orders_2 :::"Semilattice":::); let "D1", "D2" be ($#v12_waybel_0 :::"lower"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set "D1" ($#k3_yellow_4 :::""/\""::: ) "D2") -> ($#v12_waybel_0 :::"lower"::: ) ; end; theorem :: YELLOW_4:42 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k3_yellow_4 :::""/\""::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "x")) ($#k11_lattice3 :::""/\""::: ) (Set (Var "y")) ")" ) where y "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) "}" )))) ; theorem :: YELLOW_4:43 (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")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "A")) ($#k3_yellow_4 :::""/\""::: ) (Set "(" (Set (Var "B")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k3_yellow_4 :::""/\""::: ) (Set (Var "B")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "A")) ($#k3_yellow_4 :::""/\""::: ) (Set (Var "C")) ")" ))))) ; theorem :: YELLOW_4:44 (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")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "B")) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "C")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ) ($#k4_yellow_4 :::""/\""::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")) ")" ))))) ; theorem :: YELLOW_4:45 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#v12_waybel_0 :::"lower"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ) ($#k4_yellow_4 :::""/\""::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "B")) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "C")) ")" )))))) ; theorem :: YELLOW_4:46 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k3_yellow_4 :::""/\""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "x")) ($#k11_lattice3 :::""/\""::: ) (Set (Var "y")) ")" ) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: YELLOW_4:47 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k3_yellow_4 :::""/\""::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k7_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set "(" (Set (Var "x")) ($#k11_lattice3 :::""/\""::: ) (Set (Var "y")) ")" ) "," (Set "(" (Set (Var "x")) ($#k11_lattice3 :::""/\""::: ) (Set (Var "z")) ")" ) ($#k7_domain_1 :::"}"::: ) )))) ; theorem :: YELLOW_4:48 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tarski :::"c="::: ) (Set (Var "Y1"))) & (Bool (Set (Var "X2")) ($#r1_tarski :::"c="::: ) (Set (Var "Y2")))) "holds" (Bool (Set (Set (Var "X1")) ($#k3_yellow_4 :::""/\""::: ) (Set (Var "X2"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "Y1")) ($#k3_yellow_4 :::""/\""::: ) (Set (Var "Y2")))))) ; theorem :: YELLOW_4:49 (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")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "B")))))) ; theorem :: YELLOW_4:50 (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")) "," (Set (Var "B")) "being" ($#v12_waybel_0 :::"lower"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "A")) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")))))) ; theorem :: YELLOW_4:51 (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 "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set (Var "D")))))) ; theorem :: YELLOW_4:52 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "D"))) ($#r2_lattice3 :::"is_<=_than"::: ) (Set (Var "x")))))) ; theorem :: YELLOW_4:53 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "X"))) "," (Set (Var "L"))) & (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "X")) ")" )) ($#r3_orders_2 :::"<="::: ) (Set (Set (Var "x")) ($#k12_lattice3 :::""/\""::: ) (Set "(" ($#k1_yellow_0 :::"sup"::: ) (Set (Var "X")) ")" )))))) ; theorem :: YELLOW_4:54 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "A")) ($#r1_lattice3 :::"is_>=_than"::: ) (Set ($#k2_yellow_0 :::"inf"::: ) (Set "(" (Set (Var "A")) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "B")) ")" )))))) ; theorem :: YELLOW_4:55 (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")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b"))) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Set (Var "A")) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "B"))))))) ; theorem :: YELLOW_4:56 (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")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b"))) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Set (Var "A")) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "B"))))))) ; theorem :: YELLOW_4:57 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_yellow_0 :::"inf"::: ) (Set "(" (Set (Var "A")) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_yellow_0 :::"inf"::: ) (Set (Var "A")) ")" ) ($#k12_lattice3 :::""/\""::: ) (Set "(" ($#k2_yellow_0 :::"inf"::: ) (Set (Var "B")) ")" ))))) ; theorem :: YELLOW_4:58 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set (Var "L")) ")" ) ")" ) (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "y1")))) "holds" (Bool (Set (Set (Var "x")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x1")) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "y1"))))))) ; theorem :: YELLOW_4:59 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set "(" (Set (Var "X")) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "Y")) ")" )))))) ; theorem :: YELLOW_4:60 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "L")) "," (Set (Var "L")) ($#k3_yellow_3 :::":]"::: ) ) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) "{" (Set (Var "X")) where X "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) : (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k3_yellow_4 :::""/\""::: ) (Set "(" ($#k5_yellow_3 :::"proj2"::: ) (Set (Var "D")) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_yellow_3 :::"proj1"::: ) (Set (Var "D")))) ")" )) "}" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_yellow_3 :::"proj1"::: ) (Set (Var "D")) ")" ) ($#k3_yellow_4 :::""/\""::: ) (Set "(" ($#k5_yellow_3 :::"proj2"::: ) (Set (Var "D")) ")" ))))) ; theorem :: YELLOW_4:61 (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 "D1")) "," (Set (Var "D2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set "(" (Set "(" ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "D1")) ")" ) ($#k4_yellow_4 :::""/\""::: ) (Set "(" ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "D2")) ")" ) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set "(" (Set (Var "D1")) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "D2")) ")" ))))) ; theorem :: YELLOW_4:62 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set "(" (Set "(" ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "D1")) ")" ) ($#k4_yellow_4 :::""/\""::: ) (Set "(" ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "D2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set "(" (Set (Var "D1")) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "D2")) ")" ))))) ; theorem :: YELLOW_4:63 (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 "D1")) "," (Set (Var "D2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set "(" (Set "(" ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "D1")) ")" ) ($#k4_yellow_4 :::""/\""::: ) (Set "(" ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "D2")) ")" ) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set "(" (Set (Var "D1")) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "D2")) ")" ))))) ; theorem :: YELLOW_4:64 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set "(" (Set "(" ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "D1")) ")" ) ($#k4_yellow_4 :::""/\""::: ) (Set "(" ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "D2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set "(" (Set (Var "D1")) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "D2")) ")" ))))) ;