:: YELLOW_3 semantic presentation begin scheme :: YELLOW_3:sch 1 FraenkelA2{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set F2 "(" (Set (Var "s")) "," (Set (Var "t")) ")" ) where s, t "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "s")) "," (Set (Var "t"))]) "}" "is" ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" )) provided (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set F2 "(" (Set (Var "s")) "," (Set (Var "t")) ")" ) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) proof end; registrationlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set ($#k3_waybel_0 :::"downarrow"::: ) "X") -> ($#v1_xboole_0 :::"empty"::: ) ; cluster (Set ($#k4_waybel_0 :::"uparrow"::: ) "X") -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: YELLOW_3:1 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Var "D")) ($#r1_relset_1 :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "D")) ")" ) "," (Set "(" ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "D")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )))) ; theorem :: YELLOW_3:2 (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")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "c"))) & (Bool (Set (Var "b")) ($#r1_orders_2 :::"<="::: ) (Set (Var "d")))) "holds" (Bool (Set (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b"))) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "c")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "d")))))) ; theorem :: YELLOW_3: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")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "c"))) & (Bool (Set (Var "b")) ($#r1_orders_2 :::"<="::: ) (Set (Var "d")))) "holds" (Bool (Set (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b"))) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "c")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "d")))))) ; theorem :: YELLOW_3:4 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_lattice3 :::"complete"::: ) ($#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_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set "(" ($#k1_yellow_0 :::"sup"::: ) (Set (Var "D")) ")" ) ($#k12_lattice3 :::""/\""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))))) ; theorem :: YELLOW_3:5 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_lattice3 :::"complete"::: ) ($#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_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set "(" ($#k2_yellow_0 :::"inf"::: ) (Set (Var "D")) ")" ) ($#k13_lattice3 :::""\/""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))))) ; theorem :: YELLOW_3:6 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "Y")))))) ; theorem :: YELLOW_3:7 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "Y")))))) ; theorem :: YELLOW_3:8 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r3_waybel_0 :::"preserves_inf_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) )) "iff" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k12_lattice3 :::""/\""::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ))) ")" )))) ; theorem :: YELLOW_3:9 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r4_waybel_0 :::"preserves_sup_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) )) "iff" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k13_lattice3 :::""\/""::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ))) ")" )))) ; scheme :: YELLOW_3:sch 2 InfUnion{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"RelStr"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" "{" (Set "(" ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set F1 "(" ")" ) ")" ")" ) where X "is" ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "X"))]) "}" "," (Set F1 "(" ")" ) ")" ) ($#r1_orders_2 :::">="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set "(" ($#k3_tarski :::"union"::: ) "{" (Set (Var "X")) where X "is" ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "X"))]) "}" ")" ) "," (Set F1 "(" ")" ) ")" )) proof end; scheme :: YELLOW_3:sch 3 InfofInfs{ F1() -> ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" "{" (Set "(" ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set F1 "(" ")" ) ")" ")" ) where X "is" ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "X"))]) "}" "," (Set F1 "(" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set "(" ($#k3_tarski :::"union"::: ) "{" (Set (Var "X")) where X "is" ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "X"))]) "}" ")" ) "," (Set F1 "(" ")" ) ")" )) proof end; scheme :: YELLOW_3:sch 4 SupUnion{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"RelStr"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set F1 "(" ")" ) ")" ")" ) where X "is" ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "X"))]) "}" "," (Set F1 "(" ")" ) ")" ) ($#r1_orders_2 :::"<="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set "(" ($#k3_tarski :::"union"::: ) "{" (Set (Var "X")) where X "is" ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "X"))]) "}" ")" ) "," (Set F1 "(" ")" ) ")" )) proof end; scheme :: YELLOW_3:sch 5 SupofSups{ F1() -> ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" "{" (Set "(" ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set F1 "(" ")" ) ")" ")" ) where X "is" ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "X"))]) "}" "," (Set F1 "(" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set "(" ($#k3_tarski :::"union"::: ) "{" (Set (Var "X")) where X "is" ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "X"))]) "}" ")" ) "," (Set F1 "(" ")" ) ")" )) proof end; begin definitionlet "P", "R" be ($#m1_hidden :::"Relation":::); func :::"["":::"P" "," "R":::""]"::: -> ($#m1_hidden :::"Relation":::) means :: YELLOW_3:def 1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "P") & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "q")) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") ")" )) ")" )); end; :: deftheorem defines :::"[""::: YELLOW_3:def 1 : (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_3 :::"[""::: ) (Set (Var "P")) "," (Set (Var "R")) ($#k1_yellow_3 :::""]"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "q")) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" )) ")" )) ")" )); theorem :: YELLOW_3:10 (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_yellow_3 :::"[""::: ) (Set (Var "P")) "," (Set (Var "R")) ($#k1_yellow_3 :::""]"::: ) )) "iff" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "x")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "x")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ))) & (Bool "ex" (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k4_tarski :::"]"::: ) ))) & (Bool "ex" (Set (Var "e")) "," (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "e")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ))) ")" ) ")" ))) ; definitionlet "A", "B", "X", "Y" be ($#m1_hidden :::"set"::: ) ; let "P" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "A")) "," (Set (Const "B")); let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")) "," (Set (Const "Y")); :: original: :::"[""::: redefine func :::"["":::"P" "," "R":::""]"::: -> ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "X" ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) "B" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) ); end; definitionlet "X", "Y" be ($#l1_orders_2 :::"RelStr"::: ) ; func :::"[:":::"X" "," "Y":::":]"::: -> ($#v1_orders_2 :::"strict"::: ) ($#l1_orders_2 :::"RelStr"::: ) means :: YELLOW_3:def 2 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_3 :::"[""::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "X") "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "Y") ($#k2_yellow_3 :::""]"::: ) )) ")" ); end; :: deftheorem defines :::"[:"::: YELLOW_3:def 2 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "b3")) "being" ($#v1_orders_2 :::"strict"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k3_yellow_3 :::":]"::: ) )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_3 :::"[""::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "Y"))) ($#k2_yellow_3 :::""]"::: ) )) ")" ) ")" ))); definitionlet "L1", "L2" be ($#l1_orders_2 :::"RelStr"::: ) ; let "D" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Const "L1")) "," (Set (Const "L2")) ($#k3_yellow_3 :::":]"::: ) ); :: original: :::"proj1"::: redefine func :::"proj1"::: "D" -> ($#m1_subset_1 :::"Subset":::) "of" "L1"; :: original: :::"proj2"::: redefine func :::"proj2"::: "D" -> ($#m1_subset_1 :::"Subset":::) "of" "L2"; end; definitionlet "S1", "S2" be ($#l1_orders_2 :::"RelStr"::: ) ; let "D1" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "S1")); let "D2" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "S2")); :: original: :::"[:"::: redefine func :::"[:":::"D1" "," "D2":::":]"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) "S1" "," "S2" ($#k3_yellow_3 :::":]"::: ) ); end; definitionlet "S1", "S2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S1")); let "y" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S2")); :: original: :::"["::: redefine func :::"[":::"x" "," "y":::"]"::: -> ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) "S1" "," "S2" ($#k3_yellow_3 :::":]"::: ) ); end; definitionlet "L1", "L2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Const "L1")) "," (Set (Const "L2")) ($#k3_yellow_3 :::":]"::: ) ); :: original: :::"`1"::: redefine func "x" :::"`1"::: -> ($#m1_subset_1 :::"Element":::) "of" "L1"; :: original: :::"`2"::: redefine func "x" :::"`2"::: -> ($#m1_subset_1 :::"Element":::) "of" "L2"; end; theorem :: YELLOW_3:11 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "b")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S2")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "c"))) & (Bool (Set (Var "b")) ($#r1_orders_2 :::"<="::: ) (Set (Var "d"))) ")" ) "iff" (Bool (Set ($#k7_yellow_3 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k7_yellow_3 :::"]"::: ) ) ($#r1_orders_2 :::"<="::: ) (Set ($#k7_yellow_3 :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k7_yellow_3 :::"]"::: ) )) ")" )))) ; theorem :: YELLOW_3:12 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "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 ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S1")) "," (Set (Var "S2")) ($#k3_yellow_3 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) "iff" (Bool "(" (Bool (Set (Set (Var "x")) ($#k8_yellow_3 :::"`1"::: ) ) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "y")) ($#k8_yellow_3 :::"`1"::: ) )) & (Bool (Set (Set (Var "x")) ($#k9_yellow_3 :::"`2"::: ) ) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "y")) ($#k9_yellow_3 :::"`2"::: ) )) ")" ) ")" ))) ; theorem :: YELLOW_3:13 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k3_yellow_3 :::":]"::: ) ) "," (Set (Var "C")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "B")) "holds" (Bool (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))) ")" )) "holds" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set (Var "g")))))) ; registrationlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k3_yellow_3 :::"[:"::: ) "X" "," "Y" ($#k3_yellow_3 :::":]"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ; end; registrationlet "X", "Y" be ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k3_yellow_3 :::"[:"::: ) "X" "," "Y" ($#k3_yellow_3 :::":]"::: ) ) -> ($#v1_orders_2 :::"strict"::: ) ($#v3_orders_2 :::"reflexive"::: ) ; end; registrationlet "X", "Y" be ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k3_yellow_3 :::"[:"::: ) "X" "," "Y" ($#k3_yellow_3 :::":]"::: ) ) -> ($#v1_orders_2 :::"strict"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ; end; registrationlet "X", "Y" be ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k3_yellow_3 :::"[:"::: ) "X" "," "Y" ($#k3_yellow_3 :::":]"::: ) ) -> ($#v1_orders_2 :::"strict"::: ) ($#v4_orders_2 :::"transitive"::: ) ; end; registrationlet "X", "Y" be ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k3_yellow_3 :::"[:"::: ) "X" "," "Y" ($#k3_yellow_3 :::":]"::: ) ) -> ($#v1_orders_2 :::"strict"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ; end; registrationlet "X", "Y" be ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k3_yellow_3 :::"[:"::: ) "X" "," "Y" ($#k3_yellow_3 :::":]"::: ) ) -> ($#v1_orders_2 :::"strict"::: ) ($#v2_lattice3 :::"with_infima"::: ) ; end; theorem :: YELLOW_3:14 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Bool "not" (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k3_yellow_3 :::":]"::: ) ) "is" ($#v2_struct_0 :::"empty"::: ) ))) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "X")) "is" ($#v2_struct_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "Y")) "is" ($#v2_struct_0 :::"empty"::: ) )) ")" )) ; theorem :: YELLOW_3:15 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k3_yellow_3 :::":]"::: ) ) "is" ($#v3_orders_2 :::"reflexive"::: ) )) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v3_orders_2 :::"reflexive"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v3_orders_2 :::"reflexive"::: ) ) ")" )) ; theorem :: YELLOW_3:16 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k3_yellow_3 :::":]"::: ) ) "is" ($#v5_orders_2 :::"antisymmetric"::: ) )) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v5_orders_2 :::"antisymmetric"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v5_orders_2 :::"antisymmetric"::: ) ) ")" )) ; theorem :: YELLOW_3:17 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k3_yellow_3 :::":]"::: ) ) "is" ($#v4_orders_2 :::"transitive"::: ) )) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_orders_2 :::"transitive"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v4_orders_2 :::"transitive"::: ) ) ")" )) ; theorem :: YELLOW_3:18 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k3_yellow_3 :::":]"::: ) ) "is" ($#v1_lattice3 :::"with_suprema"::: ) )) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_lattice3 :::"with_suprema"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_lattice3 :::"with_suprema"::: ) ) ")" )) ; theorem :: YELLOW_3:19 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k3_yellow_3 :::":]"::: ) ) "is" ($#v2_lattice3 :::"with_infima"::: ) )) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v2_lattice3 :::"with_infima"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v2_lattice3 :::"with_infima"::: ) ) ")" )) ; definitionlet "S1", "S2" be ($#l1_orders_2 :::"RelStr"::: ) ; let "D1" be ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "S1")); let "D2" be ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "S2")); :: original: :::"[:"::: redefine func :::"[:":::"D1" "," "D2":::":]"::: -> ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) "S1" "," "S2" ($#k3_yellow_3 :::":]"::: ) ); end; theorem :: YELLOW_3:20 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S2")) "st" (Bool (Bool (Set ($#k6_yellow_3 :::"[:"::: ) (Set (Var "D1")) "," (Set (Var "D2")) ($#k6_yellow_3 :::":]"::: ) ) "is" ($#v1_waybel_0 :::"directed"::: ) )) "holds" (Bool "(" (Bool (Set (Var "D1")) "is" ($#v1_waybel_0 :::"directed"::: ) ) & (Bool (Set (Var "D2")) "is" ($#v1_waybel_0 :::"directed"::: ) ) ")" )))) ; theorem :: YELLOW_3:21 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S1")) "," (Set (Var "S2")) ($#k3_yellow_3 :::":]"::: ) ) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k4_yellow_3 :::"proj1"::: ) (Set (Var "D"))) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set ($#k5_yellow_3 :::"proj2"::: ) (Set (Var "D"))) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ))) ; theorem :: YELLOW_3:22 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S1")) "," (Set (Var "S2")) ($#k3_yellow_3 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set ($#k4_yellow_3 :::"proj1"::: ) (Set (Var "D"))) "is" ($#v1_waybel_0 :::"directed"::: ) ) & (Bool (Set ($#k5_yellow_3 :::"proj2"::: ) (Set (Var "D"))) "is" ($#v1_waybel_0 :::"directed"::: ) ) ")" ))) ; definitionlet "S1", "S2" be ($#l1_orders_2 :::"RelStr"::: ) ; let "D1" be ($#v2_waybel_0 :::"filtered"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "S1")); let "D2" be ($#v2_waybel_0 :::"filtered"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "S2")); :: original: :::"[:"::: redefine func :::"[:":::"D1" "," "D2":::":]"::: -> ($#v2_waybel_0 :::"filtered"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) "S1" "," "S2" ($#k3_yellow_3 :::":]"::: ) ); end; theorem :: YELLOW_3:23 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S2")) "st" (Bool (Bool (Set ($#k6_yellow_3 :::"[:"::: ) (Set (Var "D1")) "," (Set (Var "D2")) ($#k6_yellow_3 :::":]"::: ) ) "is" ($#v2_waybel_0 :::"filtered"::: ) )) "holds" (Bool "(" (Bool (Set (Var "D1")) "is" ($#v2_waybel_0 :::"filtered"::: ) ) & (Bool (Set (Var "D2")) "is" ($#v2_waybel_0 :::"filtered"::: ) ) ")" )))) ; theorem :: YELLOW_3:24 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_waybel_0 :::"filtered"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S1")) "," (Set (Var "S2")) ($#k3_yellow_3 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set ($#k4_yellow_3 :::"proj1"::: ) (Set (Var "D"))) "is" ($#v2_waybel_0 :::"filtered"::: ) ) & (Bool (Set ($#k5_yellow_3 :::"proj2"::: ) (Set (Var "D"))) "is" ($#v2_waybel_0 :::"filtered"::: ) ) ")" ))) ; definitionlet "S1", "S2" be ($#l1_orders_2 :::"RelStr"::: ) ; let "D1" be ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "S1")); let "D2" be ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "S2")); :: original: :::"[:"::: redefine func :::"[:":::"D1" "," "D2":::":]"::: -> ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) "S1" "," "S2" ($#k3_yellow_3 :::":]"::: ) ); end; theorem :: YELLOW_3:25 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S2")) "st" (Bool (Bool (Set ($#k6_yellow_3 :::"[:"::: ) (Set (Var "D1")) "," (Set (Var "D2")) ($#k6_yellow_3 :::":]"::: ) ) "is" ($#v13_waybel_0 :::"upper"::: ) )) "holds" (Bool "(" (Bool (Set (Var "D1")) "is" ($#v13_waybel_0 :::"upper"::: ) ) & (Bool (Set (Var "D2")) "is" ($#v13_waybel_0 :::"upper"::: ) ) ")" )))) ; theorem :: YELLOW_3:26 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S1")) "," (Set (Var "S2")) ($#k3_yellow_3 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set ($#k4_yellow_3 :::"proj1"::: ) (Set (Var "D"))) "is" ($#v13_waybel_0 :::"upper"::: ) ) & (Bool (Set ($#k5_yellow_3 :::"proj2"::: ) (Set (Var "D"))) "is" ($#v13_waybel_0 :::"upper"::: ) ) ")" ))) ; definitionlet "S1", "S2" be ($#l1_orders_2 :::"RelStr"::: ) ; let "D1" be ($#v12_waybel_0 :::"lower"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "S1")); let "D2" be ($#v12_waybel_0 :::"lower"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "S2")); :: original: :::"[:"::: redefine func :::"[:":::"D1" "," "D2":::":]"::: -> ($#v12_waybel_0 :::"lower"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) "S1" "," "S2" ($#k3_yellow_3 :::":]"::: ) ); end; theorem :: YELLOW_3:27 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S2")) "st" (Bool (Bool (Set ($#k6_yellow_3 :::"[:"::: ) (Set (Var "D1")) "," (Set (Var "D2")) ($#k6_yellow_3 :::":]"::: ) ) "is" ($#v12_waybel_0 :::"lower"::: ) )) "holds" (Bool "(" (Bool (Set (Var "D1")) "is" ($#v12_waybel_0 :::"lower"::: ) ) & (Bool (Set (Var "D2")) "is" ($#v12_waybel_0 :::"lower"::: ) ) ")" )))) ; theorem :: YELLOW_3:28 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v12_waybel_0 :::"lower"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S1")) "," (Set (Var "S2")) ($#k3_yellow_3 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set ($#k4_yellow_3 :::"proj1"::: ) (Set (Var "D"))) "is" ($#v12_waybel_0 :::"lower"::: ) ) & (Bool (Set ($#k5_yellow_3 :::"proj2"::: ) (Set (Var "D"))) "is" ($#v12_waybel_0 :::"lower"::: ) ) ")" ))) ; definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; attr "R" is :::"void"::: means :: YELLOW_3:def 3 (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "R") "is" ($#v1_xboole_0 :::"empty"::: ) ); end; :: deftheorem defines :::"void"::: YELLOW_3:def 3 : (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_yellow_3 :::"void"::: ) ) "iff" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )); registration cluster ($#v2_struct_0 :::"empty"::: ) -> ($#v1_yellow_3 :::"void"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) bbbadV2_ORDERS_2() ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#~v1_yellow_3 "non" ($#v1_yellow_3 :::"void"::: ) ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registration cluster ($#~v1_yellow_3 "non" ($#v1_yellow_3 :::"void"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) -> ($#~v1_yellow_3 "non" ($#v1_yellow_3 :::"void"::: ) ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registrationlet "R" be ($#~v1_yellow_3 "non" ($#v1_yellow_3 :::"void"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "R") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: YELLOW_3:29 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S2")) "st" (Bool (Bool (Set ($#k7_yellow_3 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_yellow_3 :::"]"::: ) ) ($#r2_lattice3 :::"is_>=_than"::: ) (Set ($#k6_yellow_3 :::"[:"::: ) (Set (Var "D1")) "," (Set (Var "D2")) ($#k6_yellow_3 :::":]"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "D1"))) & (Bool (Set (Var "y")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "D2"))) ")" )))))) ; theorem :: YELLOW_3:30 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "D2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S2")) "st" (Bool (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "D1"))) & (Bool (Set (Var "y")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "D2")))) "holds" (Bool (Set ($#k7_yellow_3 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_yellow_3 :::"]"::: ) ) ($#r2_lattice3 :::"is_>=_than"::: ) (Set ($#k6_yellow_3 :::"[:"::: ) (Set (Var "D1")) "," (Set (Var "D2")) ($#k6_yellow_3 :::":]"::: ) ))))))) ; theorem :: YELLOW_3:31 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "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 "S1")) "," (Set (Var "S2")) ($#k3_yellow_3 :::":]"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S2")) "holds" (Bool "(" (Bool (Set ($#k7_yellow_3 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_yellow_3 :::"]"::: ) ) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "D"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set ($#k4_yellow_3 :::"proj1"::: ) (Set (Var "D")))) & (Bool (Set (Var "y")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set ($#k5_yellow_3 :::"proj2"::: ) (Set (Var "D")))) ")" ) ")" ))))) ; theorem :: YELLOW_3:32 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S2")) "st" (Bool (Bool (Set ($#k7_yellow_3 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_yellow_3 :::"]"::: ) ) ($#r1_lattice3 :::"is_<=_than"::: ) (Set ($#k6_yellow_3 :::"[:"::: ) (Set (Var "D1")) "," (Set (Var "D2")) ($#k6_yellow_3 :::":]"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "D1"))) & (Bool (Set (Var "y")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "D2"))) ")" )))))) ; theorem :: YELLOW_3:33 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "D2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S2")) "st" (Bool (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "D1"))) & (Bool (Set (Var "y")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "D2")))) "holds" (Bool (Set ($#k7_yellow_3 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_yellow_3 :::"]"::: ) ) ($#r1_lattice3 :::"is_<=_than"::: ) (Set ($#k6_yellow_3 :::"[:"::: ) (Set (Var "D1")) "," (Set (Var "D2")) ($#k6_yellow_3 :::":]"::: ) ))))))) ; theorem :: YELLOW_3:34 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "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 "S1")) "," (Set (Var "S2")) ($#k3_yellow_3 :::":]"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S2")) "holds" (Bool "(" (Bool (Set ($#k7_yellow_3 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_yellow_3 :::"]"::: ) ) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "D"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set ($#k4_yellow_3 :::"proj1"::: ) (Set (Var "D")))) & (Bool (Set (Var "y")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set ($#k5_yellow_3 :::"proj2"::: ) (Set (Var "D")))) ")" ) ")" ))))) ; theorem :: YELLOW_3:35 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "D2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S2")) "st" (Bool (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "D1")) "," (Set (Var "S1"))) & (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "D2")) "," (Set (Var "S2"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S1")) "," (Set (Var "S2")) ($#k3_yellow_3 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set ($#k6_yellow_3 :::"[:"::: ) (Set (Var "D1")) "," (Set (Var "D2")) ($#k6_yellow_3 :::":]"::: ) ))) "holds" (Bool (Set ($#k7_yellow_3 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_yellow_3 :::"]"::: ) ) ($#r1_orders_2 :::"<="::: ) (Set (Var "b"))) ")" )) "holds" (Bool "(" (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S1")) "st" (Bool (Bool (Set (Var "c")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "D1")))) "holds" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "c"))) ")" ) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S2")) "st" (Bool (Bool (Set (Var "d")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "D2")))) "holds" (Bool (Set (Var "y")) ($#r1_orders_2 :::"<="::: ) (Set (Var "d"))) ")" ) ")" )))))) ; theorem :: YELLOW_3:36 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "D2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S2")) "st" (Bool (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "D1")) "," (Set (Var "S1"))) & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "D2")) "," (Set (Var "S2"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S1")) "," (Set (Var "S2")) ($#k3_yellow_3 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set ($#k6_yellow_3 :::"[:"::: ) (Set (Var "D1")) "," (Set (Var "D2")) ($#k6_yellow_3 :::":]"::: ) ))) "holds" (Bool (Set ($#k7_yellow_3 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_yellow_3 :::"]"::: ) ) ($#r1_orders_2 :::">="::: ) (Set (Var "b"))) ")" )) "holds" (Bool "(" (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S1")) "st" (Bool (Bool (Set (Var "c")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "D1")))) "holds" (Bool (Set (Var "x")) ($#r1_orders_2 :::">="::: ) (Set (Var "c"))) ")" ) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S2")) "st" (Bool (Bool (Set (Var "d")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "D2")))) "holds" (Bool (Set (Var "y")) ($#r1_orders_2 :::">="::: ) (Set (Var "d"))) ")" ) ")" )))))) ; theorem :: YELLOW_3:37 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S2")) "st" (Bool (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S1")) "st" (Bool (Bool (Set (Var "c")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "D1")))) "holds" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "c"))) ")" ) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S2")) "st" (Bool (Bool (Set (Var "d")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "D2")))) "holds" (Bool (Set (Var "y")) ($#r1_orders_2 :::"<="::: ) (Set (Var "d"))) ")" )) "holds" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S1")) "," (Set (Var "S2")) ($#k3_yellow_3 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set ($#k6_yellow_3 :::"[:"::: ) (Set (Var "D1")) "," (Set (Var "D2")) ($#k6_yellow_3 :::":]"::: ) ))) "holds" (Bool (Set ($#k7_yellow_3 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_yellow_3 :::"]"::: ) ) ($#r1_orders_2 :::"<="::: ) (Set (Var "b"))))))))) ; theorem :: YELLOW_3:38 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S2")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S2")) "st" (Bool (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S1")) "st" (Bool (Bool (Set (Var "c")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "D1")))) "holds" (Bool (Set (Var "x")) ($#r1_orders_2 :::">="::: ) (Set (Var "c"))) ")" ) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S2")) "st" (Bool (Bool (Set (Var "d")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "D2")))) "holds" (Bool (Set (Var "y")) ($#r1_orders_2 :::">="::: ) (Set (Var "d"))) ")" )) "holds" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S1")) "," (Set (Var "S2")) ($#k3_yellow_3 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set ($#k6_yellow_3 :::"[:"::: ) (Set (Var "D1")) "," (Set (Var "D2")) ($#k6_yellow_3 :::":]"::: ) ))) "holds" (Bool (Set ($#k7_yellow_3 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_yellow_3 :::"]"::: ) ) ($#r1_orders_2 :::">="::: ) (Set (Var "b"))))))))) ; theorem :: YELLOW_3:39 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S2")) "holds" (Bool "(" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "D1")) "," (Set (Var "S1"))) & (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "D2")) "," (Set (Var "S2"))) ")" ) "iff" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set ($#k6_yellow_3 :::"[:"::: ) (Set (Var "D1")) "," (Set (Var "D2")) ($#k6_yellow_3 :::":]"::: ) ) "," (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S1")) "," (Set (Var "S2")) ($#k3_yellow_3 :::":]"::: ) )) ")" )))) ; theorem :: YELLOW_3:40 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S2")) "holds" (Bool "(" (Bool "(" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "D1")) "," (Set (Var "S1"))) & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "D2")) "," (Set (Var "S2"))) ")" ) "iff" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set ($#k6_yellow_3 :::"[:"::: ) (Set (Var "D1")) "," (Set (Var "D2")) ($#k6_yellow_3 :::":]"::: ) ) "," (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S1")) "," (Set (Var "S2")) ($#k3_yellow_3 :::":]"::: ) )) ")" )))) ; theorem :: YELLOW_3:41 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S1")) "," (Set (Var "S2")) ($#k3_yellow_3 :::":]"::: ) ) "holds" (Bool "(" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set ($#k4_yellow_3 :::"proj1"::: ) (Set (Var "D"))) "," (Set (Var "S1"))) & (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set ($#k5_yellow_3 :::"proj2"::: ) (Set (Var "D"))) "," (Set (Var "S2"))) ")" ) "iff" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "D")) "," (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S1")) "," (Set (Var "S2")) ($#k3_yellow_3 :::":]"::: ) )) ")" ))) ; theorem :: YELLOW_3:42 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S1")) "," (Set (Var "S2")) ($#k3_yellow_3 :::":]"::: ) ) "holds" (Bool "(" (Bool "(" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set ($#k4_yellow_3 :::"proj1"::: ) (Set (Var "D"))) "," (Set (Var "S1"))) & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set ($#k5_yellow_3 :::"proj2"::: ) (Set (Var "D"))) "," (Set (Var "S2"))) ")" ) "iff" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "D")) "," (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S1")) "," (Set (Var "S2")) ($#k3_yellow_3 :::":]"::: ) )) ")" ))) ; theorem :: YELLOW_3:43 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S2")) "st" (Bool (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "D1")) "," (Set (Var "S1"))) & (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "D2")) "," (Set (Var "S2")))) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set ($#k6_yellow_3 :::"[:"::: ) (Set (Var "D1")) "," (Set (Var "D2")) ($#k6_yellow_3 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k7_yellow_3 :::"["::: ) (Set "(" ($#k1_yellow_0 :::"sup"::: ) (Set (Var "D1")) ")" ) "," (Set "(" ($#k1_yellow_0 :::"sup"::: ) (Set (Var "D2")) ")" ) ($#k7_yellow_3 :::"]"::: ) ))))) ; theorem :: YELLOW_3:44 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S2")) "st" (Bool (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "D1")) "," (Set (Var "S1"))) & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "D2")) "," (Set (Var "S2")))) "holds" (Bool (Set ($#k2_yellow_0 :::"inf"::: ) (Set ($#k6_yellow_3 :::"[:"::: ) (Set (Var "D1")) "," (Set (Var "D2")) ($#k6_yellow_3 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k7_yellow_3 :::"["::: ) (Set "(" ($#k2_yellow_0 :::"inf"::: ) (Set (Var "D1")) ")" ) "," (Set "(" ($#k2_yellow_0 :::"inf"::: ) (Set (Var "D2")) ")" ) ($#k7_yellow_3 :::"]"::: ) ))))) ; registrationlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k3_yellow_3 :::"[:"::: ) "X" "," "Y" ($#k3_yellow_3 :::":]"::: ) ) -> ($#v1_orders_2 :::"strict"::: ) ($#v3_lattice3 :::"complete"::: ) ; end; theorem :: YELLOW_3:45 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k3_yellow_3 :::":]"::: ) ) "is" ($#v3_lattice3 :::"complete"::: ) )) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v3_lattice3 :::"complete"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v3_lattice3 :::"complete"::: ) ) ")" )) ; theorem :: YELLOW_3:46 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "L1")) "," (Set (Var "L2")) ($#k3_yellow_3 :::":]"::: ) ) "st" (Bool (Bool "(" (Bool (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "L1")) "," (Set (Var "L2")) ($#k3_yellow_3 :::":]"::: ) ) "is" ($#v3_lattice3 :::"complete"::: ) ) "or" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "D")) "," (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "L1")) "," (Set (Var "L2")) ($#k3_yellow_3 :::":]"::: ) )) ")" )) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k7_yellow_3 :::"["::: ) (Set "(" ($#k1_yellow_0 :::"sup"::: ) (Set "(" ($#k4_yellow_3 :::"proj1"::: ) (Set (Var "D")) ")" ) ")" ) "," (Set "(" ($#k1_yellow_0 :::"sup"::: ) (Set "(" ($#k5_yellow_3 :::"proj2"::: ) (Set (Var "D")) ")" ) ")" ) ($#k7_yellow_3 :::"]"::: ) )))) ; theorem :: YELLOW_3:47 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "L1")) "," (Set (Var "L2")) ($#k3_yellow_3 :::":]"::: ) ) "st" (Bool (Bool "(" (Bool (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "L1")) "," (Set (Var "L2")) ($#k3_yellow_3 :::":]"::: ) ) "is" ($#v3_lattice3 :::"complete"::: ) ) "or" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "D")) "," (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "L1")) "," (Set (Var "L2")) ($#k3_yellow_3 :::":]"::: ) )) ")" )) "holds" (Bool (Set ($#k2_yellow_0 :::"inf"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k7_yellow_3 :::"["::: ) (Set "(" ($#k2_yellow_0 :::"inf"::: ) (Set "(" ($#k4_yellow_3 :::"proj1"::: ) (Set (Var "D")) ")" ) ")" ) "," (Set "(" ($#k2_yellow_0 :::"inf"::: ) (Set "(" ($#k5_yellow_3 :::"proj2"::: ) (Set (Var "D")) ")" ) ")" ) ($#k7_yellow_3 :::"]"::: ) )))) ; theorem :: YELLOW_3:48 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S1")) "," (Set (Var "S2")) ($#k3_yellow_3 :::":]"::: ) ) "holds" (Bool (Set ($#k6_yellow_3 :::"[:"::: ) (Set "(" ($#k4_yellow_3 :::"proj1"::: ) (Set (Var "D")) ")" ) "," (Set "(" ($#k5_yellow_3 :::"proj2"::: ) (Set (Var "D")) ")" ) ($#k6_yellow_3 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "D")))))) ; theorem :: YELLOW_3:49 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_waybel_0 :::"filtered"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S1")) "," (Set (Var "S2")) ($#k3_yellow_3 :::":]"::: ) ) "holds" (Bool (Set ($#k6_yellow_3 :::"[:"::: ) (Set "(" ($#k4_yellow_3 :::"proj1"::: ) (Set (Var "D")) ")" ) "," (Set "(" ($#k5_yellow_3 :::"proj2"::: ) (Set (Var "D")) ")" ) ($#k6_yellow_3 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "D")))))) ; scheme :: YELLOW_3:sch 6 Kappa2DS{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) , F2() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) , F3() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k3_yellow_3 :::"[:"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#k3_yellow_3 :::":]"::: ) ) "," (Set F3 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set F2 "(" ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))))) provided (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set F2 "(" ")" ) "holds" (Bool (Set F4 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) "is" ($#m1_subset_1 :::"Element":::) "of" (Set F3 "(" ")" )))) proof end;