:: YELLOW_0 semantic presentation begin scheme :: YELLOW_0:sch 1 RelStrEx{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b"))) "iff" (Bool P1[(Set (Var "a")) "," (Set (Var "b"))]) ")" ) ")" ) ")" )) proof end; definitionlet "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; redefine attr "A" is :::"reflexive"::: means :: YELLOW_0:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "A" "holds" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "x")))); end; :: deftheorem defines :::"reflexive"::: YELLOW_0:def 1 : (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_orders_2 :::"reflexive"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "holds" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "x")))) ")" )); definitionlet "A" be ($#l1_orders_2 :::"RelStr"::: ) ; redefine attr "A" is :::"transitive"::: means :: YELLOW_0:def 2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "A" "st" (Bool (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) & (Bool (Set (Var "y")) ($#r1_orders_2 :::"<="::: ) (Set (Var "z")))) "holds" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "z")))); redefine attr "A" is :::"antisymmetric"::: means :: YELLOW_0:def 3 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "A" "st" (Bool (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) & (Bool (Set (Var "y")) ($#r1_orders_2 :::"<="::: ) (Set (Var "x")))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))); end; :: deftheorem defines :::"transitive"::: YELLOW_0:def 2 : (Bool "for" (Set (Var "A")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_orders_2 :::"transitive"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) & (Bool (Set (Var "y")) ($#r1_orders_2 :::"<="::: ) (Set (Var "z")))) "holds" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "z")))) ")" )); :: deftheorem defines :::"antisymmetric"::: YELLOW_0:def 3 : (Bool "for" (Set (Var "A")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v5_orders_2 :::"antisymmetric"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) & (Bool (Set (Var "y")) ($#r1_orders_2 :::"<="::: ) (Set (Var "x")))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v3_orders_2 :::"reflexive"::: ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_lattice3 :::"complete"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registrationlet "x" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k1_tarski :::"{"::: ) (Set (Const "x")) ($#k1_tarski :::"}"::: ) ); cluster (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) "," "R" "#)" ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ; end; registration cluster (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v1_orders_2 :::"strict"::: ) ($#v3_orders_2 :::"reflexive"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; theorem :: YELLOW_0:1 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P2"))) "#)" ))) "holds" (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P1")) (Bool "for" (Set (Var "a2")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P2")) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Var "b2")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a1")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b1")))) "implies" (Bool (Set (Var "a2")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b2"))) ")" & "(" (Bool (Bool (Set (Var "a1")) ($#r2_orders_2 :::"<"::: ) (Set (Var "b1")))) "implies" (Bool (Set (Var "a2")) ($#r2_orders_2 :::"<"::: ) (Set (Var "b2"))) ")" ")" )))) ; theorem :: YELLOW_0:2 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P2"))) "#)" ))) "holds" (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P1")) (Bool "for" (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "P2")) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a2")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "X")) ($#r2_lattice3 :::"is_<=_than"::: ) (Set (Var "a1")))) "implies" (Bool (Set (Var "X")) ($#r2_lattice3 :::"is_<=_than"::: ) (Set (Var "a2"))) ")" & "(" (Bool (Bool (Set (Var "X")) ($#r1_lattice3 :::"is_>=_than"::: ) (Set (Var "a1")))) "implies" (Bool (Set (Var "X")) ($#r1_lattice3 :::"is_>=_than"::: ) (Set (Var "a2"))) ")" ")" ))))) ; theorem :: YELLOW_0:3 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P2"))) "#)" )) & (Bool (Set (Var "P1")) "is" ($#v3_lattice3 :::"complete"::: ) )) "holds" (Bool (Set (Var "P2")) "is" ($#v3_lattice3 :::"complete"::: ) )) ; theorem :: YELLOW_0:4 (Bool "for" (Set (Var "L")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y")))) "holds" (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "y")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X")))) "implies" (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X"))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X")))) "implies" (Bool (Set (Var "y")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X"))) ")" ")" )))) ; theorem :: YELLOW_0:5 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X")))) "implies" (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))))) "implies" (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X"))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X")))) "implies" (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))))) "implies" (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X"))) ")" ")" )))) ; theorem :: YELLOW_0:6 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_lattice3 :::"is_<=_than"::: ) (Set (Var "a"))) & (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r1_lattice3 :::"is_>=_than"::: ) (Set (Var "a"))) ")" ))) ; theorem :: YELLOW_0:7 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "b")) ($#k1_tarski :::"}"::: ) ))) "implies" (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b"))) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b")))) "implies" (Bool (Set (Var "a")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "b")) ($#k1_tarski :::"}"::: ) )) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "b")) ($#k1_tarski :::"}"::: ) ))) "implies" (Bool (Set (Var "b")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a"))) ")" & "(" (Bool (Bool (Set (Var "b")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a")))) "implies" (Bool (Set (Var "a")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "b")) ($#k1_tarski :::"}"::: ) )) ")" ")" ))) ; theorem :: YELLOW_0:8 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k2_tarski :::"}"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "c"))) ")" ) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "c")))) "implies" (Bool (Set (Var "a")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k2_tarski :::"}"::: ) )) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k2_tarski :::"}"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a"))) & (Bool (Set (Var "c")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a"))) ")" ) ")" & "(" (Bool (Bool (Set (Var "b")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a"))) & (Bool (Set (Var "c")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a")))) "implies" (Bool (Set (Var "a")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k2_tarski :::"}"::: ) )) ")" ")" ))) ; theorem :: YELLOW_0:9 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "Y")))) "implies" (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X"))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "Y")))) "implies" (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X"))) ")" ")" )))) ; theorem :: YELLOW_0:10 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "Y")))) "implies" (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "Y")))) "implies" (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")))) ")" ")" )))) ; theorem :: YELLOW_0:11 (Bool "for" (Set (Var "L")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r2_lattice3 :::"is_<=_than"::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "X")) ($#r2_lattice3 :::"is_<=_than"::: ) (Set (Var "y")))))) ; theorem :: YELLOW_0:12 (Bool "for" (Set (Var "L")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r1_lattice3 :::"is_>=_than"::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_orders_2 :::">="::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "X")) ($#r1_lattice3 :::"is_>=_than"::: ) (Set (Var "y")))))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k2_struct_0 :::"[#]"::: ) "L") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; begin definitionlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; attr "L" is :::"lower-bounded"::: means :: YELLOW_0:def 4 (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))); attr "L" is :::"upper-bounded"::: means :: YELLOW_0:def 5 (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))); end; :: deftheorem defines :::"lower-bounded"::: YELLOW_0:def 4 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_yellow_0 :::"lower-bounded"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))))) ")" )); :: deftheorem defines :::"upper-bounded"::: YELLOW_0:def 5 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v2_yellow_0 :::"upper-bounded"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))))) ")" )); definitionlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; attr "L" is :::"bounded"::: means :: YELLOW_0:def 6 (Bool "(" (Bool "L" "is" ($#v1_yellow_0 :::"lower-bounded"::: ) ) & (Bool "L" "is" ($#v2_yellow_0 :::"upper-bounded"::: ) ) ")" ); end; :: deftheorem defines :::"bounded"::: YELLOW_0:def 6 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v3_yellow_0 :::"bounded"::: ) ) "iff" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_yellow_0 :::"lower-bounded"::: ) ) & (Bool (Set (Var "L")) "is" ($#v2_yellow_0 :::"upper-bounded"::: ) ) ")" ) ")" )); theorem :: YELLOW_0:13 (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "P2"))) "#)" ))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "P1")) "is" ($#v1_yellow_0 :::"lower-bounded"::: ) )) "implies" (Bool (Set (Var "P2")) "is" ($#v1_yellow_0 :::"lower-bounded"::: ) ) ")" & "(" (Bool (Bool (Set (Var "P1")) "is" ($#v2_yellow_0 :::"upper-bounded"::: ) )) "implies" (Bool (Set (Var "P2")) "is" ($#v2_yellow_0 :::"upper-bounded"::: ) ) ")" ")" )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_yellow_0 :::"bounded"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v3_yellow_0 :::"bounded"::: ) -> ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v2_yellow_0 :::"upper-bounded"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v2_yellow_0 :::"upper-bounded"::: ) -> ($#v3_yellow_0 :::"bounded"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) bbbadV2_ORDERS_2() ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_lattice3 :::"complete"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; definitionlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#m1_hidden :::"set"::: ) ; pred :::"ex_sup_of"::: "X" "," "L" means :: YELLOW_0:def 7 (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool "(" (Bool "X" ($#r2_lattice3 :::"is_<=_than"::: ) (Set (Var "a"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool "X" ($#r2_lattice3 :::"is_<=_than"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "b")) ($#r1_orders_2 :::">="::: ) (Set (Var "a"))) ")" ) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool "X" ($#r2_lattice3 :::"is_<=_than"::: ) (Set (Var "c"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool "X" ($#r2_lattice3 :::"is_<=_than"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "b")) ($#r1_orders_2 :::">="::: ) (Set (Var "c"))) ")" )) "holds" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ) ")" )); pred :::"ex_inf_of"::: "X" "," "L" means :: YELLOW_0:def 8 (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool "(" (Bool "X" ($#r1_lattice3 :::"is_>=_than"::: ) (Set (Var "a"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool "X" ($#r1_lattice3 :::"is_>=_than"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "b")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a"))) ")" ) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool "X" ($#r1_lattice3 :::"is_>=_than"::: ) (Set (Var "c"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool "X" ($#r1_lattice3 :::"is_>=_than"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "b")) ($#r1_orders_2 :::"<="::: ) (Set (Var "c"))) ")" )) "holds" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ) ")" )); end; :: deftheorem defines :::"ex_sup_of"::: YELLOW_0:def 7 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "X")) ($#r2_lattice3 :::"is_<=_than"::: ) (Set (Var "a"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r2_lattice3 :::"is_<=_than"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "b")) ($#r1_orders_2 :::">="::: ) (Set (Var "a"))) ")" ) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r2_lattice3 :::"is_<=_than"::: ) (Set (Var "c"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r2_lattice3 :::"is_<=_than"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "b")) ($#r1_orders_2 :::">="::: ) (Set (Var "c"))) ")" )) "holds" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ) ")" )) ")" ))); :: deftheorem defines :::"ex_inf_of"::: YELLOW_0:def 8 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "X")) ($#r1_lattice3 :::"is_>=_than"::: ) (Set (Var "a"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r1_lattice3 :::"is_>=_than"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "b")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a"))) ")" ) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r1_lattice3 :::"is_>=_than"::: ) (Set (Var "c"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r1_lattice3 :::"is_>=_than"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "b")) ($#r1_orders_2 :::"<="::: ) (Set (Var "c"))) ")" )) "holds" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ) ")" )) ")" ))); theorem :: YELLOW_0:14 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L2"))) "#)" ))) "holds" (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L1")))) "implies" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L2"))) ")" & "(" (Bool (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L1")))) "implies" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L2"))) ")" ")" ))) ; theorem :: YELLOW_0:15 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "X")) ($#r2_lattice3 :::"is_<=_than"::: ) (Set (Var "a"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r2_lattice3 :::"is_<=_than"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b"))) ")" ) ")" )) ")" ))) ; theorem :: YELLOW_0:16 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "X")) ($#r1_lattice3 :::"is_>=_than"::: ) (Set (Var "a"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r1_lattice3 :::"is_>=_than"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "a")) ($#r1_orders_2 :::">="::: ) (Set (Var "b"))) ")" ) ")" )) ")" ))) ; theorem :: YELLOW_0:17 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) ")" ))) ; theorem :: YELLOW_0:18 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k10_lattice3 :::""\/""::: ) (Set (Var "b")))) & (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) ) "," (Set (Var "L"))) "iff" (Bool "(" (Bool (Set (Var "c")) ($#r1_orders_2 :::">="::: ) (Set (Var "a"))) & (Bool (Set (Var "c")) ($#r1_orders_2 :::">="::: ) (Set (Var "b"))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "d")) ($#r1_orders_2 :::">="::: ) (Set (Var "a"))) & (Bool (Set (Var "d")) ($#r1_orders_2 :::">="::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "c")) ($#r1_orders_2 :::"<="::: ) (Set (Var "d"))) ")" ) ")" ) ")" ))) ; theorem :: YELLOW_0:19 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k11_lattice3 :::""/\""::: ) (Set (Var "b")))) & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) ) "," (Set (Var "L"))) "iff" (Bool "(" (Bool (Set (Var "c")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a"))) & (Bool (Set (Var "c")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b"))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "d")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a"))) & (Bool (Set (Var "d")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "c")) ($#r1_orders_2 :::">="::: ) (Set (Var "d"))) ")" ) ")" ) ")" ))) ; theorem :: YELLOW_0:20 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_lattice3 :::"with_suprema"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) ) "," (Set (Var "L")))) ")" )) ; theorem :: YELLOW_0:21 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v2_lattice3 :::"with_infima"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) ) "," (Set (Var "L")))) ")" )) ; theorem :: YELLOW_0:22 (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")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b")))) "iff" (Bool "(" (Bool (Set (Var "c")) ($#r1_orders_2 :::">="::: ) (Set (Var "a"))) & (Bool (Set (Var "c")) ($#r1_orders_2 :::">="::: ) (Set (Var "b"))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "d")) ($#r1_orders_2 :::">="::: ) (Set (Var "a"))) & (Bool (Set (Var "d")) ($#r1_orders_2 :::">="::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "c")) ($#r1_orders_2 :::"<="::: ) (Set (Var "d"))) ")" ) ")" ) ")" ))) ; theorem :: YELLOW_0:23 (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")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b")))) "iff" (Bool "(" (Bool (Set (Var "c")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a"))) & (Bool (Set (Var "c")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b"))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "d")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a"))) & (Bool (Set (Var "d")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "c")) ($#r1_orders_2 :::">="::: ) (Set (Var "d"))) ")" ) ")" ) ")" ))) ; theorem :: YELLOW_0:24 (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")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b")))) "iff" (Bool (Set (Var "a")) ($#r1_orders_2 :::">="::: ) (Set (Var "b"))) ")" ))) ; theorem :: YELLOW_0:25 (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 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b")))) "iff" (Bool (Set (Var "a")) ($#r3_orders_2 :::"<="::: ) (Set (Var "b"))) ")" ))) ; definitionlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#m1_hidden :::"set"::: ) ; func :::""\/""::: "(" "X" "," "L" ")" -> ($#m1_subset_1 :::"Element":::) "of" "L" means :: YELLOW_0:def 9 (Bool "(" (Bool "X" ($#r2_lattice3 :::"is_<=_than"::: ) it) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool "X" ($#r2_lattice3 :::"is_<=_than"::: ) (Set (Var "a")))) "holds" (Bool it ($#r1_orders_2 :::"<="::: ) (Set (Var "a"))) ")" ) ")" ) if (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) "X" "," "L") ; func :::""/\""::: "(" "X" "," "L" ")" -> ($#m1_subset_1 :::"Element":::) "of" "L" means :: YELLOW_0:def 10 (Bool "(" (Bool "X" ($#r1_lattice3 :::"is_>=_than"::: ) it) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool "X" ($#r1_lattice3 :::"is_>=_than"::: ) (Set (Var "a")))) "holds" (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) it) ")" ) ")" ) if (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) "X" "," "L") ; end; :: deftheorem defines :::""\/""::: YELLOW_0:def 9 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" )) "iff" (Bool "(" (Bool (Set (Var "X")) ($#r2_lattice3 :::"is_<=_than"::: ) (Set (Var "b3"))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r2_lattice3 :::"is_<=_than"::: ) (Set (Var "a")))) "holds" (Bool (Set (Var "b3")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a"))) ")" ) ")" ) ")" )))); :: deftheorem defines :::""/\""::: YELLOW_0:def 10 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" )) "iff" (Bool "(" (Bool (Set (Var "X")) ($#r1_lattice3 :::"is_>=_than"::: ) (Set (Var "b3"))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r1_lattice3 :::"is_>=_than"::: ) (Set (Var "a")))) "holds" (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b3"))) ")" ) ")" ) ")" )))); theorem :: YELLOW_0:26 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L2"))) "#)" ))) "holds" (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L1")))) "holds" (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "L1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "L2")) ")" )))) ; theorem :: YELLOW_0:27 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L2"))) "#)" ))) "holds" (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L1")))) "holds" (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "L1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "L2")) ")" )))) ; theorem :: YELLOW_0: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 "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k15_lattice3 :::""\/""::: ) "(" (Set (Var "X")) "," (Set "(" ($#k14_lattice3 :::"latt"::: ) (Set (Var "L")) ")" ) ")" )) & (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k16_lattice3 :::""/\""::: ) "(" (Set (Var "X")) "," (Set "(" ($#k14_lattice3 :::"latt"::: ) (Set (Var "L")) ")" ) ")" )) ")" ))) ; theorem :: YELLOW_0:29 (Bool "for" (Set (Var "L")) "being" ($#v4_lattice3 :::"complete"::: ) ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k15_lattice3 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set "(" ($#k3_lattice3 :::"LattPOSet"::: ) (Set (Var "L")) ")" ) ")" )) & (Bool (Set ($#k16_lattice3 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set "(" ($#k3_lattice3 :::"LattPOSet"::: ) (Set (Var "L")) ")" ) ")" )) ")" ))) ; theorem :: YELLOW_0:30 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" )) & (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "b")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b"))) ")" ) ")" ) ")" )))) ; theorem :: YELLOW_0:31 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" )) & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "b")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "a")) ($#r1_orders_2 :::">="::: ) (Set (Var "b"))) ")" ) ")" ) ")" )))) ; theorem :: YELLOW_0:32 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" )) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "b")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b"))) ")" ) ")" ) ")" )))) ; theorem :: YELLOW_0:33 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" )) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "b")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "a")) ($#r1_orders_2 :::">="::: ) (Set (Var "b"))) ")" ) ")" ) ")" )))) ; theorem :: YELLOW_0:34 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) & (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "Y")) "," (Set (Var "L")))) "holds" (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) ($#r1_orders_2 :::"<="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" )))) ; theorem :: YELLOW_0:35 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "Y")) "," (Set (Var "L")))) "holds" (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) ($#r1_orders_2 :::">="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" )))) ; theorem :: YELLOW_0:36 (Bool "for" (Set (Var "L")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) & (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "Y")) "," (Set (Var "L"))) & (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y"))) "," (Set (Var "L")))) "holds" (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "L")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ")" ) ($#k10_lattice3 :::""\/""::: ) (Set "(" ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" ")" ))))) ; theorem :: YELLOW_0:37 (Bool "for" (Set (Var "L")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "Y")) "," (Set (Var "L"))) & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y"))) "," (Set (Var "L")))) "holds" (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "L")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ")" ) ($#k11_lattice3 :::""/\""::: ) (Set "(" ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" ")" ))))) ; notationlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); synonym :::"sup"::: "X" for :::""\/""::: "(" "X" "," "L" ")" ; synonym :::"inf"::: "X" for :::""/\""::: "(" "X" "," "L" ")" ; end; theorem :: YELLOW_0:38 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ) "," (Set (Var "L"))) & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ) "," (Set (Var "L"))) ")" ))) ; theorem :: YELLOW_0:39 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k2_yellow_0 :::"inf"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ))) ; theorem :: YELLOW_0:40 (Bool "for" (Set (Var "L")) "being" ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_yellow_0 :::"inf"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k7_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b")))))) ; theorem :: YELLOW_0:41 (Bool "for" (Set (Var "L")) "being" ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k7_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b")))))) ; theorem :: YELLOW_0:42 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "L"))) & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set (Var "L"))) ")" )) ; theorem :: YELLOW_0:43 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "L"))) & (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set (Var "L"))) ")" )) ; definitionlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; func :::"Bottom"::: "L" -> ($#m1_subset_1 :::"Element":::) "of" "L" equals :: YELLOW_0:def 11 (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," "L" ")" ); func :::"Top"::: "L" -> ($#m1_subset_1 :::"Element":::) "of" "L" equals :: YELLOW_0:def 12 (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," "L" ")" ); end; :: deftheorem defines :::"Bottom"::: YELLOW_0:def 11 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "L")) ")" ))); :: deftheorem defines :::"Top"::: YELLOW_0:def 12 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k4_yellow_0 :::"Top"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "L")) ")" ))); theorem :: YELLOW_0:44 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L"))) ($#r1_orders_2 :::"<="::: ) (Set (Var "x"))))) ; theorem :: YELLOW_0:45 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set ($#k4_yellow_0 :::"Top"::: ) (Set (Var "L")))))) ; theorem :: YELLOW_0: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_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X"))) "iff" (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "Y"))) ")" ) ")" ) & (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) "holds" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "Y")) "," (Set (Var "L"))))) ; theorem :: YELLOW_0: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")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X"))) "iff" (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "Y"))) ")" ) ")" )) "holds" (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" )))) ; theorem :: YELLOW_0:48 (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_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X"))) "iff" (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "Y"))) ")" ) ")" ) & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) "holds" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "Y")) "," (Set (Var "L"))))) ; theorem :: YELLOW_0:49 (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_hidden :::"set"::: ) "st" (Bool (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X"))) "iff" (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "Y"))) ")" ) ")" )) "holds" (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" )))) ; theorem :: YELLOW_0:50 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) "implies" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) "," (Set (Var "L"))) ")" & "(" (Bool (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) "," (Set (Var "L")))) "implies" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) ")" & "(" (Bool (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) "implies" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) "," (Set (Var "L"))) ")" & "(" (Bool (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) "," (Set (Var "L")))) "implies" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) ")" ")" ))) ; theorem :: YELLOW_0:51 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) "or" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) "," (Set (Var "L"))) ")" )) "holds" (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ")" ) "," (Set (Var "L")) ")" )))) ; theorem :: YELLOW_0:52 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) "or" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) "," (Set (Var "L"))) ")" )) "holds" (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ")" ) "," (Set (Var "L")) ")" )))) ; theorem :: YELLOW_0:53 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) ")" )) "holds" (Bool (Set (Var "L")) "is" ($#v3_lattice3 :::"complete"::: ) )) ; theorem :: YELLOW_0:54 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_lattice3 :::"with_suprema"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) ")" )) ; theorem :: YELLOW_0:55 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v2_lattice3 :::"with_infima"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) ")" )) ; begin definitionlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; mode :::"SubRelStr"::: "of" "L" -> ($#l1_orders_2 :::"RelStr"::: ) means :: YELLOW_0:def 13 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" it) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "L")) ")" ); end; :: deftheorem defines :::"SubRelStr"::: YELLOW_0:def 13 : (Bool "for" (Set (Var "L")) "," (Set (Var "b2")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L"))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "b2"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L")))) ")" ) ")" )); definitionlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Const "L")); attr "S" is :::"full"::: means :: YELLOW_0:def 14 (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "S") ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "L") ($#k1_toler_1 :::"|_2"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S"))); end; :: deftheorem defines :::"full"::: YELLOW_0:def 14 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v4_yellow_0 :::"full"::: ) ) "iff" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L"))) ($#k1_toler_1 :::"|_2"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) ")" ))); registrationlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_orders_2 :::"strict"::: ) ($#v4_yellow_0 :::"full"::: ) for ($#m1_yellow_0 :::"SubRelStr"::: ) "of" "L"; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v4_yellow_0 :::"full"::: ) for ($#m1_yellow_0 :::"SubRelStr"::: ) "of" "L"; end; theorem :: YELLOW_0:56 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set (Var "X")) "," (Set "(" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L"))) ($#k1_toler_1 :::"|_2"::: ) (Set (Var "X")) ")" ) "#)" ) "is" ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L"))))) ; theorem :: YELLOW_0:57 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))))) "holds" (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "S1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "S2"))) "#)" )))) ; definitionlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); func :::"subrelstr"::: "X" -> ($#v1_orders_2 :::"strict"::: ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" "L" means :: YELLOW_0:def 15 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) "X"); end; :: deftheorem defines :::"subrelstr"::: YELLOW_0:def 15 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b3")) "being" ($#v1_orders_2 :::"strict"::: ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "X")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) ")" )))); theorem :: YELLOW_0:58 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")))))) ; theorem :: YELLOW_0:59 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b"))))))) ; theorem :: YELLOW_0:60 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) "holds" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))))))) ; theorem :: YELLOW_0:61 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X")))) "implies" (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X"))) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X")))) "implies" (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X"))) ")" ")" )))))) ; theorem :: YELLOW_0:62 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X")))) "implies" (Bool (Set (Var "a")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X"))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X")))) "implies" (Bool (Set (Var "a")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X"))) ")" ")" )))))) ; registrationlet "L" be ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v4_yellow_0 :::"full"::: ) -> ($#v3_orders_2 :::"reflexive"::: ) ($#v4_yellow_0 :::"full"::: ) for ($#m1_yellow_0 :::"SubRelStr"::: ) "of" "L"; end; registrationlet "L" be ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v4_yellow_0 :::"full"::: ) -> ($#v4_orders_2 :::"transitive"::: ) ($#v4_yellow_0 :::"full"::: ) for ($#m1_yellow_0 :::"SubRelStr"::: ) "of" "L"; end; registrationlet "L" be ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v4_yellow_0 :::"full"::: ) -> ($#v5_orders_2 :::"antisymmetric"::: ) ($#v4_yellow_0 :::"full"::: ) for ($#m1_yellow_0 :::"SubRelStr"::: ) "of" "L"; end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Const "L")); attr "S" is :::"meet-inheriting"::: means :: YELLOW_0:def 16 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S")) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S")) & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ) "," "L")) "holds" (Bool (Set ($#k2_yellow_0 :::"inf"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) )) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S"))); attr "S" is :::"join-inheriting"::: means :: YELLOW_0:def 17 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S")) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S")) & (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ) "," "L")) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) )) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S"))); end; :: deftheorem defines :::"meet-inheriting"::: YELLOW_0:def 16 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v5_yellow_0 :::"meet-inheriting"::: ) ) "iff" (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 "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "L")))) "holds" (Bool (Set ($#k2_yellow_0 :::"inf"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) )) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) ")" ))); :: deftheorem defines :::"join-inheriting"::: YELLOW_0:def 17 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v6_yellow_0 :::"join-inheriting"::: ) ) "iff" (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 "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "L")))) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) )) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) ")" ))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Const "L")); attr "S" is :::"infs-inheriting"::: means :: YELLOW_0:def 18 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" "S" "st" (Bool (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," "L")) "holds" (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," "L" ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S"))); attr "S" is :::"sups-inheriting"::: means :: YELLOW_0:def 19 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" "S" "st" (Bool (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," "L")) "holds" (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," "L" ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S"))); end; :: deftheorem defines :::"infs-inheriting"::: YELLOW_0:def 18 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v7_yellow_0 :::"infs-inheriting"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (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")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) ")" ))); :: deftheorem defines :::"sups-inheriting"::: YELLOW_0:def 19 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v8_yellow_0 :::"sups-inheriting"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) "holds" (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) ")" ))); registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v7_yellow_0 :::"infs-inheriting"::: ) -> ($#v5_yellow_0 :::"meet-inheriting"::: ) for ($#m1_yellow_0 :::"SubRelStr"::: ) "of" "L"; cluster ($#v8_yellow_0 :::"sups-inheriting"::: ) -> ($#v6_yellow_0 :::"join-inheriting"::: ) for ($#m1_yellow_0 :::"SubRelStr"::: ) "of" "L"; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#v4_yellow_0 :::"full"::: ) ($#v7_yellow_0 :::"infs-inheriting"::: ) ($#v8_yellow_0 :::"sups-inheriting"::: ) for ($#m1_yellow_0 :::"SubRelStr"::: ) "of" "L"; end; theorem :: YELLOW_0:63 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) & (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) "holds" (Bool "(" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "S"))) & (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "S")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" )) ")" )))) ; theorem :: YELLOW_0:64 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) & (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) "holds" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "S"))) & (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "S")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" )) ")" )))) ; theorem :: YELLOW_0:65 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "L"))) & (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "L")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) "holds" (Bool "(" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "S"))) & (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "S")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "L")) ")" )) ")" )))) ; theorem :: YELLOW_0:66 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "L"))) & (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "L")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) "holds" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "S"))) & (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "S")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "L")) ")" )) ")" )))) ; registrationlet "L" be ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#v5_yellow_0 :::"meet-inheriting"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_lattice3 :::"with_infima"::: ) ($#v4_yellow_0 :::"full"::: ) ($#v5_yellow_0 :::"meet-inheriting"::: ) for ($#m1_yellow_0 :::"SubRelStr"::: ) "of" "L"; end; registrationlet "L" be ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#v6_yellow_0 :::"join-inheriting"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v4_yellow_0 :::"full"::: ) ($#v6_yellow_0 :::"join-inheriting"::: ) for ($#m1_yellow_0 :::"SubRelStr"::: ) "of" "L"; end; theorem :: YELLOW_0:67 (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 "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) "holds" (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "S")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ))))) ; theorem :: YELLOW_0:68 (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 "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) "holds" (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "S")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ))))) ; theorem :: YELLOW_0:69 (Bool "for" (Set (Var "L")) "being" ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#v5_yellow_0 :::"meet-inheriting"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "x")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "b")))))))) ; theorem :: YELLOW_0:70 (Bool "for" (Set (Var "L")) "being" ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#v6_yellow_0 :::"join-inheriting"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "x")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "b")))))))) ;