:: WAYBEL_4 semantic presentation begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; func "L" :::"-waybelow"::: -> ($#m1_subset_1 :::"Relation":::) "of" "L" means :: WAYBEL_4:def 1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "y"))) ")" )); end; :: deftheorem defines :::"-waybelow"::: WAYBEL_4:def 1 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k1_waybel_4 :::"-waybelow"::: ) )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "x")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "y"))) ")" )) ")" ))); definitionlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; func :::"IntRel"::: "L" -> ($#m1_subset_1 :::"Relation":::) "of" "L" equals :: WAYBEL_4:def 2 (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "L"); end; :: deftheorem defines :::"IntRel"::: WAYBEL_4:def 2 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k2_waybel_4 :::"IntRel"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L"))))); definitionlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "L")); attr "R" is :::"auxiliary(i)"::: means :: WAYBEL_4:def 3 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R")) "holds" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y")))); attr "R" is :::"auxiliary(ii)"::: means :: WAYBEL_4:def 4 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool (Set (Var "u")) ($#r1_orders_2 :::"<="::: ) (Set (Var "x"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") & (Bool (Set (Var "y")) ($#r1_orders_2 :::"<="::: ) (Set (Var "z")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "u")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R")); end; :: deftheorem defines :::"auxiliary(i)"::: WAYBEL_4:def 3 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_waybel_4 :::"auxiliary(i)"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "holds" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y")))) ")" ))); :: deftheorem defines :::"auxiliary(ii)"::: WAYBEL_4:def 4 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v2_waybel_4 :::"auxiliary(ii)"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "u")) ($#r1_orders_2 :::"<="::: ) (Set (Var "x"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "y")) ($#r1_orders_2 :::"<="::: ) (Set (Var "z")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "u")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) ")" ))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "L")); attr "R" is :::"auxiliary(iii)"::: means :: WAYBEL_4:def 5 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R")) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "x")) ($#k10_lattice3 :::""\/""::: ) (Set (Var "y")) ")" ) "," (Set (Var "z")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R")); attr "R" is :::"auxiliary(iv)"::: means :: WAYBEL_4:def 6 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) "L" ")" ) "," (Set (Var "x")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R")); end; :: deftheorem defines :::"auxiliary(iii)"::: WAYBEL_4:def 5 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v3_waybel_4 :::"auxiliary(iii)"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "x")) ($#k10_lattice3 :::""\/""::: ) (Set (Var "y")) ")" ) "," (Set (Var "z")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) ")" ))); :: deftheorem defines :::"auxiliary(iv)"::: WAYBEL_4:def 6 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v4_waybel_4 :::"auxiliary(iv)"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")) ")" ) "," (Set (Var "x")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) ")" ))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "L")); attr "R" is :::"auxiliary"::: means :: WAYBEL_4:def 7 (Bool "(" (Bool "R" "is" ($#v1_waybel_4 :::"auxiliary(i)"::: ) ) & (Bool "R" "is" ($#v2_waybel_4 :::"auxiliary(ii)"::: ) ) & (Bool "R" "is" ($#v3_waybel_4 :::"auxiliary(iii)"::: ) ) & (Bool "R" "is" ($#v4_waybel_4 :::"auxiliary(iv)"::: ) ) ")" ); end; :: deftheorem defines :::"auxiliary"::: WAYBEL_4:def 7 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v5_waybel_4 :::"auxiliary"::: ) ) "iff" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_waybel_4 :::"auxiliary(i)"::: ) ) & (Bool (Set (Var "R")) "is" ($#v2_waybel_4 :::"auxiliary(ii)"::: ) ) & (Bool (Set (Var "R")) "is" ($#v3_waybel_4 :::"auxiliary(iii)"::: ) ) & (Bool (Set (Var "R")) "is" ($#v4_waybel_4 :::"auxiliary(iv)"::: ) ) ")" ) ")" ))); registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v5_waybel_4 :::"auxiliary"::: ) -> ($#v1_waybel_4 :::"auxiliary(i)"::: ) ($#v2_waybel_4 :::"auxiliary(ii)"::: ) ($#v3_waybel_4 :::"auxiliary(iii)"::: ) ($#v4_waybel_4 :::"auxiliary(iv)"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") ($#k2_zfmisc_1 :::":]"::: ) )); cluster ($#v1_waybel_4 :::"auxiliary(i)"::: ) ($#v2_waybel_4 :::"auxiliary(ii)"::: ) ($#v3_waybel_4 :::"auxiliary(iii)"::: ) ($#v4_waybel_4 :::"auxiliary(iv)"::: ) -> ($#v5_waybel_4 :::"auxiliary"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "L" be ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v5_waybel_4 :::"auxiliary"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: WAYBEL_4:1 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "AR")) "being" ($#v2_waybel_4 :::"auxiliary(ii)"::: ) ($#v3_waybel_4 :::"auxiliary(iii)"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "AR"))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y")) "," (Set (Var "u")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "AR")))) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "x")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "y")) ")" ) "," (Set "(" (Set (Var "z")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "u")) ")" ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "AR")))))) ; registrationlet "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); cluster ($#v1_waybel_4 :::"auxiliary(i)"::: ) ($#v2_waybel_4 :::"auxiliary(ii)"::: ) -> ($#v8_relat_2 :::"transitive"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k2_waybel_4 :::"IntRel"::: ) "L") -> ($#v1_waybel_4 :::"auxiliary(i)"::: ) ; end; registrationlet "L" be ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k2_waybel_4 :::"IntRel"::: ) "L") -> ($#v2_waybel_4 :::"auxiliary(ii)"::: ) ; end; registrationlet "L" be ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k2_waybel_4 :::"IntRel"::: ) "L") -> ($#v3_waybel_4 :::"auxiliary(iii)"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k2_waybel_4 :::"IntRel"::: ) "L") -> ($#v4_waybel_4 :::"auxiliary(iv)"::: ) ; end; definitionlet "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); func :::"Aux"::: "L" -> ($#m1_hidden :::"set"::: ) means :: WAYBEL_4:def 8 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "a")) "is" ($#v5_waybel_4 :::"auxiliary"::: ) ($#m1_subset_1 :::"Relation":::) "of" "L") ")" )); end; :: deftheorem defines :::"Aux"::: WAYBEL_4:def 8 : (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_waybel_4 :::"Aux"::: ) (Set (Var "L")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "a")) "is" ($#v5_waybel_4 :::"auxiliary"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L"))) ")" )) ")" ))); registrationlet "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); cluster (Set ($#k3_waybel_4 :::"Aux"::: ) "L") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: WAYBEL_4:2 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "AR")) "being" ($#v1_waybel_4 :::"auxiliary(i)"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "AR")) ($#r1_relset_1 :::"c="::: ) (Set ($#k2_waybel_4 :::"IntRel"::: ) (Set (Var "L")))))) ; theorem :: WAYBEL_4:3 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) "holds" (Bool (Set ($#k4_yellow_0 :::"Top"::: ) (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k3_waybel_4 :::"Aux"::: ) (Set (Var "L")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_waybel_4 :::"IntRel"::: ) (Set (Var "L"))))) ; registrationlet "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); cluster (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k3_waybel_4 :::"Aux"::: ) "L" ")" )) -> ($#v2_yellow_0 :::"upper-bounded"::: ) ; end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; func :::"AuxBottom"::: "L" -> ($#m1_subset_1 :::"Relation":::) "of" "L" means :: WAYBEL_4:def 9 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) "L")) ")" )); end; :: deftheorem defines :::"AuxBottom"::: WAYBEL_4:def 9 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_waybel_4 :::"AuxBottom"::: ) (Set (Var "L")))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")))) ")" )) ")" ))); registrationlet "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); cluster (Set ($#k4_waybel_4 :::"AuxBottom"::: ) "L") -> ($#v5_waybel_4 :::"auxiliary"::: ) ; end; theorem :: WAYBEL_4:4 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "AR")) "being" ($#v4_waybel_4 :::"auxiliary(iv)"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k4_waybel_4 :::"AuxBottom"::: ) (Set (Var "L"))) ($#r1_relset_1 :::"c="::: ) (Set (Var "AR"))))) ; theorem :: WAYBEL_4:5 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) "holds" (Bool (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k3_waybel_4 :::"Aux"::: ) (Set (Var "L")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_waybel_4 :::"AuxBottom"::: ) (Set (Var "L"))))) ; registrationlet "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); cluster (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k3_waybel_4 :::"Aux"::: ) "L" ")" )) -> ($#v1_yellow_0 :::"lower-bounded"::: ) ; end; theorem :: WAYBEL_4:6 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_waybel_4 :::"auxiliary(i)"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "b"))) "is" ($#v1_waybel_4 :::"auxiliary(i)"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L"))))) ; theorem :: WAYBEL_4:7 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v2_waybel_4 :::"auxiliary(ii)"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "b"))) "is" ($#v2_waybel_4 :::"auxiliary(ii)"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L"))))) ; theorem :: WAYBEL_4:8 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v3_waybel_4 :::"auxiliary(iii)"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "b"))) "is" ($#v3_waybel_4 :::"auxiliary(iii)"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L"))))) ; theorem :: WAYBEL_4:9 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v4_waybel_4 :::"auxiliary(iv)"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "b"))) "is" ($#v4_waybel_4 :::"auxiliary(iv)"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L"))))) ; theorem :: WAYBEL_4:10 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v5_waybel_4 :::"auxiliary"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "b"))) "is" ($#v5_waybel_4 :::"auxiliary"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L"))))) ; theorem :: WAYBEL_4:11 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k3_waybel_4 :::"Aux"::: ) (Set (Var "L")) ")" ) ")" ) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "X"))) "is" ($#v5_waybel_4 :::"auxiliary"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L"))))) ; registrationlet "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); cluster (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k3_waybel_4 :::"Aux"::: ) "L" ")" )) -> ($#v2_lattice3 :::"with_infima"::: ) ; end; registrationlet "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); cluster (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k3_waybel_4 :::"Aux"::: ) "L" ")" )) -> ($#v3_lattice3 :::"complete"::: ) ; end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); let "AR" be ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "L"))); func "AR" :::"-below"::: "x" -> ($#m1_subset_1 :::"Subset":::) "of" "L" equals :: WAYBEL_4:def 10 "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Element":::) "of" "L" : (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y")) "," "x" ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "AR") "}" ; func "AR" :::"-above"::: "x" -> ($#m1_subset_1 :::"Subset":::) "of" "L" equals :: WAYBEL_4:def 11 "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Element":::) "of" "L" : (Bool (Set ($#k1_domain_1 :::"["::: ) "x" "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "AR") "}" ; end; :: deftheorem defines :::"-below"::: WAYBEL_4:def 10 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "AR")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "holds" (Bool (Set (Set (Var "AR")) ($#k5_waybel_4 :::"-below"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "AR"))) "}" )))); :: deftheorem defines :::"-above"::: WAYBEL_4:def 11 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "AR")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "holds" (Bool (Set (Set (Var "AR")) ($#k6_waybel_4 :::"-above"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "AR"))) "}" )))); theorem :: WAYBEL_4:12 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "AR")) "being" ($#v1_waybel_4 :::"auxiliary(i)"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "AR")) ($#k5_waybel_4 :::"-below"::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x"))))))) ; registrationlet "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); let "AR" be ($#v4_waybel_4 :::"auxiliary(iv)"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "L")); cluster (Set "AR" ($#k5_waybel_4 :::"-below"::: ) "x") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); let "AR" be ($#v2_waybel_4 :::"auxiliary(ii)"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "L")); cluster (Set "AR" ($#k5_waybel_4 :::"-below"::: ) "x") -> ($#v12_waybel_0 :::"lower"::: ) ; end; registrationlet "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); let "AR" be ($#v3_waybel_4 :::"auxiliary(iii)"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "L")); cluster (Set "AR" ($#k5_waybel_4 :::"-below"::: ) "x") -> ($#v1_waybel_0 :::"directed"::: ) ; end; definitionlet "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); let "AR" be ($#v2_waybel_4 :::"auxiliary(ii)"::: ) ($#v3_waybel_4 :::"auxiliary(iii)"::: ) ($#v4_waybel_4 :::"auxiliary(iv)"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "L")); func "AR" :::"-below"::: -> ($#m1_subset_1 :::"Function":::) "of" "L" "," (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) "L" ")" ) ")" ) means :: WAYBEL_4:def 12 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "AR" ($#k5_waybel_4 :::"-below"::: ) (Set (Var "x"))))); end; :: deftheorem defines :::"-below"::: WAYBEL_4:def 12 : (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "AR")) "being" ($#v2_waybel_4 :::"auxiliary(ii)"::: ) ($#v3_waybel_4 :::"auxiliary(iii)"::: ) ($#v4_waybel_4 :::"auxiliary(iv)"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set (Var "L")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "AR")) ($#k7_waybel_4 :::"-below"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "AR")) ($#k5_waybel_4 :::"-below"::: ) (Set (Var "x"))))) ")" )))); theorem :: WAYBEL_4:13 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "AR")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "AR")) ($#k5_waybel_4 :::"-below"::: ) (Set (Var "y")))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "AR"))) ")" ))))) ; theorem :: WAYBEL_4:14 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "AR")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "AR")) ($#k6_waybel_4 :::"-above"::: ) (Set (Var "y")))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "AR"))) ")" ))))) ; theorem :: WAYBEL_4:15 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "AR")) "being" ($#v1_waybel_4 :::"auxiliary(i)"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "AR")) ($#r2_relset_1 :::"="::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L"))))) "holds" (Bool (Set (Set (Var "AR")) ($#k5_waybel_4 :::"-below"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x"))))))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); func :::"MonSet"::: "L" -> ($#v1_orders_2 :::"strict"::: ) ($#l1_orders_2 :::"RelStr"::: ) means :: WAYBEL_4:def 13 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it))) "implies" (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Function":::) "of" "L" "," (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) "L" ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set (Var "s")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set (Set (Var "s")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x")))) ")" ) ")" )) ")" & "(" (Bool (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Function":::) "of" "L" "," (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) "L" ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set (Var "s")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set (Set (Var "s")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x")))) ")" ) ")" ))) "implies" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it)) ")" & (Bool "(" "for" (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" it)) "iff" (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" "L" "," (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) "L" ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it)) & (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it)) & (Bool (Set (Var "f")) ($#r1_yellow_2 :::"<="::: ) (Set (Var "g"))) ")" )) ")" ) ")" ) ")" )); end; :: deftheorem defines :::"MonSet"::: WAYBEL_4:def 13 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "b2")) "being" ($#v1_orders_2 :::"strict"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k8_waybel_4 :::"MonSet"::: ) (Set (Var "L")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))))) "implies" (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set (Var "L")) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set (Var "s")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "s")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x")))) ")" ) ")" )) ")" & "(" (Bool (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set (Var "L")) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set (Var "s")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "s")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x")))) ")" ) ")" ))) "implies" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2")))) ")" & (Bool "(" "for" (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "b2")))) "iff" (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set (Var "L")) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2")))) & (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2")))) & (Bool (Set (Var "f")) ($#r1_yellow_2 :::"<="::: ) (Set (Var "g"))) ")" )) ")" ) ")" ) ")" )) ")" ))); theorem :: WAYBEL_4:16 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) "holds" (Bool (Set ($#k8_waybel_4 :::"MonSet"::: ) (Set (Var "L"))) "is" ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set (Var "L")) ")" ) ")" ) ($#k6_yellow_1 :::"|^"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))))) ; theorem :: WAYBEL_4:17 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "AR")) "being" ($#v2_waybel_4 :::"auxiliary(ii)"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "AR")) ($#k5_waybel_4 :::"-below"::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "AR")) ($#k5_waybel_4 :::"-below"::: ) (Set (Var "y"))))))) ; registrationlet "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); let "AR" be ($#v2_waybel_4 :::"auxiliary(ii)"::: ) ($#v3_waybel_4 :::"auxiliary(iii)"::: ) ($#v4_waybel_4 :::"auxiliary(iv)"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "L")); cluster (Set "AR" ($#k7_waybel_4 :::"-below"::: ) ) -> ($#v5_orders_3 :::"monotone"::: ) ; end; theorem :: WAYBEL_4:18 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "AR")) "being" ($#v5_waybel_4 :::"auxiliary"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "AR")) ($#k7_waybel_4 :::"-below"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k8_waybel_4 :::"MonSet"::: ) (Set (Var "L")) ")" ))))) ; registrationlet "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); cluster (Set ($#k8_waybel_4 :::"MonSet"::: ) "L") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ; end; theorem :: WAYBEL_4:19 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) "holds" (Bool (Set ($#k3_yellow_2 :::"IdsMap"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k8_waybel_4 :::"MonSet"::: ) (Set (Var "L")) ")" )))) ; theorem :: WAYBEL_4:20 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "AR")) "being" ($#v5_waybel_4 :::"auxiliary"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "AR")) ($#k7_waybel_4 :::"-below"::: ) ) ($#r1_yellow_2 :::"<="::: ) (Set ($#k3_yellow_2 :::"IdsMap"::: ) (Set (Var "L")))))) ; theorem :: WAYBEL_4:21 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set (Var "I"))))) ; theorem :: WAYBEL_4:22 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k4_yellow_0 :::"Top"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set (Var "F"))))) ; theorem :: WAYBEL_4:23 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"Poset":::) "holds" (Bool (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")) ")" ) ($#k6_domain_1 :::"}"::: ) ))) ; theorem :: WAYBEL_4:24 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"Poset":::) "holds" (Bool (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set "(" ($#k4_yellow_0 :::"Top"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_yellow_0 :::"Top"::: ) (Set (Var "L")) ")" ) ($#k6_domain_1 :::"}"::: ) ))) ; theorem :: WAYBEL_4:25 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) "holds" (Bool (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")) ")" ) ($#k6_domain_1 :::"}"::: ) )) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set (Var "L")) ")" ) ")" ))) ; theorem :: WAYBEL_4:26 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) "holds" (Bool (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k8_waybel_4 :::"MonSet"::: ) (Set (Var "L")) ")" )))) ; theorem :: WAYBEL_4:27 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "AR")) "being" ($#v5_waybel_4 :::"auxiliary"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k3_yellow_0 :::"Bottom"::: ) (Set (Var "L")) ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" ) "," (Set "(" (Set (Var "AR")) ($#k7_waybel_4 :::"-below"::: ) ")" ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" ($#k8_waybel_4 :::"MonSet"::: ) (Set (Var "L")) ")" ))))) ; registrationlet "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); cluster (Set ($#k8_waybel_4 :::"MonSet"::: ) "L") -> ($#v1_orders_2 :::"strict"::: ) ($#v2_yellow_0 :::"upper-bounded"::: ) ; end; definitionlet "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); func :::"Rel2Map"::: "L" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k3_waybel_4 :::"Aux"::: ) "L" ")" ) ")" ) "," (Set "(" ($#k8_waybel_4 :::"MonSet"::: ) "L" ")" ) means :: WAYBEL_4:def 14 (Bool "for" (Set (Var "AR")) "being" ($#v5_waybel_4 :::"auxiliary"::: ) ($#m1_subset_1 :::"Relation":::) "of" "L" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "AR"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "AR")) ($#k7_waybel_4 :::"-below"::: ) ))); end; :: deftheorem defines :::"Rel2Map"::: WAYBEL_4:def 14 : (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k3_waybel_4 :::"Aux"::: ) (Set (Var "L")) ")" ) ")" ) "," (Set "(" ($#k8_waybel_4 :::"MonSet"::: ) (Set (Var "L")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k9_waybel_4 :::"Rel2Map"::: ) (Set (Var "L")))) "iff" (Bool "for" (Set (Var "AR")) "being" ($#v5_waybel_4 :::"auxiliary"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "AR"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "AR")) ($#k7_waybel_4 :::"-below"::: ) ))) ")" ))); theorem :: WAYBEL_4:28 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#v5_waybel_4 :::"auxiliary"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "R1")) ($#r1_relset_1 :::"c="::: ) (Set (Var "R2")))) "holds" (Bool (Set (Set (Var "R1")) ($#k7_waybel_4 :::"-below"::: ) ) ($#r1_yellow_2 :::"<="::: ) (Set (Set (Var "R2")) ($#k7_waybel_4 :::"-below"::: ) )))) ; theorem :: WAYBEL_4:29 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "R1")) ($#r1_relset_1 :::"c="::: ) (Set (Var "R2")))) "holds" (Bool (Set (Set (Var "R1")) ($#k5_waybel_4 :::"-below"::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R2")) ($#k5_waybel_4 :::"-below"::: ) (Set (Var "x"))))))) ; registrationlet "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); cluster (Set ($#k9_waybel_4 :::"Rel2Map"::: ) "L") -> ($#v5_orders_3 :::"monotone"::: ) ; end; definitionlet "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); func :::"Map2Rel"::: "L" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k8_waybel_4 :::"MonSet"::: ) "L" ")" ) "," (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k3_waybel_4 :::"Aux"::: ) "L" ")" ) ")" ) means :: WAYBEL_4:def 15 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k8_waybel_4 :::"MonSet"::: ) "L" ")" )))) "holds" (Bool "ex" (Set (Var "AR")) "being" ($#v5_waybel_4 :::"auxiliary"::: ) ($#m1_subset_1 :::"Relation":::) "of" "L" "st" (Bool "(" (Bool (Set (Var "AR")) ($#r1_hidden :::"="::: ) (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) & (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 "AR"))) "iff" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element":::) "of" "L"(Bool "ex" (Set (Var "s9")) "being" ($#m1_subset_1 :::"Function":::) "of" "L" "," (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) "L" ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "x9")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "y9")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "s9")) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set (Var "x9")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "s9")) ($#k3_funct_2 :::"."::: ) (Set (Var "y9")))) ")" ))) ")" ) ")" ) ")" ))); end; :: deftheorem defines :::"Map2Rel"::: WAYBEL_4:def 15 : (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k8_waybel_4 :::"MonSet"::: ) (Set (Var "L")) ")" ) "," (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k3_waybel_4 :::"Aux"::: ) (Set (Var "L")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k10_waybel_4 :::"Map2Rel"::: ) (Set (Var "L")))) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k8_waybel_4 :::"MonSet"::: ) (Set (Var "L")) ")" )))) "holds" (Bool "ex" (Set (Var "AR")) "being" ($#v5_waybel_4 :::"auxiliary"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "AR")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) & (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 "AR"))) "iff" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))(Bool "ex" (Set (Var "s9")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set (Var "L")) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "x9")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "y9")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "s9")) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set (Var "x9")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "s9")) ($#k3_funct_2 :::"."::: ) (Set (Var "y9")))) ")" ))) ")" ) ")" ) ")" ))) ")" ))); registrationlet "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); cluster (Set ($#k10_waybel_4 :::"Map2Rel"::: ) "L") -> ($#v5_orders_3 :::"monotone"::: ) ; end; theorem :: WAYBEL_4:30 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) "holds" (Bool (Set (Set "(" ($#k10_waybel_4 :::"Map2Rel"::: ) (Set (Var "L")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k9_waybel_4 :::"Rel2Map"::: ) (Set (Var "L")) ")" )) ($#r1_funct_2 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k9_waybel_4 :::"Rel2Map"::: ) (Set (Var "L")) ")" ) ")" )))) ; theorem :: WAYBEL_4:31 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) "holds" (Bool (Set (Set "(" ($#k9_waybel_4 :::"Rel2Map"::: ) (Set (Var "L")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k10_waybel_4 :::"Map2Rel"::: ) (Set (Var "L")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k8_waybel_4 :::"MonSet"::: ) (Set (Var "L")) ")" ))))) ; registrationlet "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::); cluster (Set ($#k9_waybel_4 :::"Rel2Map"::: ) "L") -> bbbadV2_FUNCT_1() ; end; theorem :: WAYBEL_4:32 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) "holds" (Bool (Set (Set "(" ($#k9_waybel_4 :::"Rel2Map"::: ) (Set (Var "L")) ")" ) ($#k2_funct_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k10_waybel_4 :::"Map2Rel"::: ) (Set (Var "L"))))) ; theorem :: WAYBEL_4:33 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"sup-Semilattice":::) "holds" (Bool (Set ($#k9_waybel_4 :::"Rel2Map"::: ) (Set (Var "L"))) "is" ($#v23_waybel_0 :::"isomorphic"::: ) )) ; theorem :: WAYBEL_4:34 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "I")) where I "is" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) : (Bool (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "I")))) "}" ) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel_3 :::"waybelow"::: ) (Set (Var "x")))))) ; definitionlet "L" be ($#l1_orders_2 :::"Semilattice":::); let "I" be ($#m1_subset_1 :::"Ideal":::) "of" (Set (Const "L")); func :::"DownMap"::: "I" -> ($#m1_subset_1 :::"Function":::) "of" "L" "," (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) "L" ")" ) ")" ) means :: WAYBEL_4:def 16 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) "I"))) "implies" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x")) ")" ) ($#k9_subset_1 :::"/\"::: ) "I")) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) "I")))) "implies" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x")))) ")" ")" )); end; :: deftheorem defines :::"DownMap"::: WAYBEL_4:def 16 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set (Var "L")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k11_waybel_4 :::"DownMap"::: ) (Set (Var "I")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "I"))))) "implies" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "I")))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "I")))))) "implies" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x")))) ")" ")" )) ")" )))); theorem :: WAYBEL_4:35 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k11_waybel_4 :::"DownMap"::: ) (Set (Var "I"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k8_waybel_4 :::"MonSet"::: ) (Set (Var "L")) ")" ))))) ; theorem :: WAYBEL_4:36 (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 "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v12_waybel_0 :::"lower"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k4_yellow_4 :::""/\""::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "D"))))))) ; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "AR" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "L")); attr "AR" is :::"approximating"::: means :: WAYBEL_4:def 17 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" "AR" ($#k5_waybel_4 :::"-below"::: ) (Set (Var "x")) ")" )))); end; :: deftheorem defines :::"approximating"::: WAYBEL_4:def 17 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "AR")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "AR")) "is" ($#v6_waybel_4 :::"approximating"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" (Set (Var "AR")) ($#k5_waybel_4 :::"-below"::: ) (Set (Var "x")) ")" )))) ")" ))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::); let "mp" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "L")) "," (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set (Const "L")) ")" ) ")" ); attr "mp" is :::"approximating"::: means :: WAYBEL_4:def 18 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" (Bool "ex" (Set (Var "ii")) "being" ($#m1_subset_1 :::"Subset":::) "of" "L" "st" (Bool "(" (Bool (Set (Var "ii")) ($#r1_hidden :::"="::: ) (Set "mp" ($#k3_funct_2 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "ii")))) ")" ))); end; :: deftheorem defines :::"approximating"::: WAYBEL_4:def 18 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "mp")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set (Var "L")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "mp")) "is" ($#v7_waybel_4 :::"approximating"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "ex" (Set (Var "ii")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "ii")) ($#r1_hidden :::"="::: ) (Set (Set (Var "mp")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "ii")))) ")" ))) ")" ))); theorem :: WAYBEL_4:37 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v2_waybel_2 :::"meet-continuous"::: ) ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k11_waybel_4 :::"DownMap"::: ) (Set (Var "I"))) "is" ($#v7_waybel_4 :::"approximating"::: ) ))) ; theorem :: WAYBEL_4:38 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool (Set (Var "L")) "is" ($#v2_waybel_2 :::"meet-continuous"::: ) )) ; registration cluster ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v3_waybel_3 :::"continuous"::: ) -> ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v2_waybel_2 :::"meet-continuous"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; theorem :: WAYBEL_4:39 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k11_waybel_4 :::"DownMap"::: ) (Set (Var "I"))) "is" ($#v7_waybel_4 :::"approximating"::: ) ))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "L" ($#k1_waybel_4 :::"-waybelow"::: ) ) -> ($#v1_waybel_4 :::"auxiliary(i)"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "L" ($#k1_waybel_4 :::"-waybelow"::: ) ) -> ($#v2_waybel_4 :::"auxiliary(ii)"::: ) ; end; registrationlet "L" be ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"Poset":::); cluster (Set "L" ($#k1_waybel_4 :::"-waybelow"::: ) ) -> ($#v3_waybel_4 :::"auxiliary(iii)"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v25_waybel_0 :::"/\-complete"::: ) ($#l1_orders_2 :::"Poset":::); cluster (Set "L" ($#k1_waybel_4 :::"-waybelow"::: ) ) -> ($#v3_waybel_4 :::"auxiliary(iii)"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "L" ($#k1_waybel_4 :::"-waybelow"::: ) ) -> ($#v4_waybel_4 :::"auxiliary(iv)"::: ) ; end; theorem :: WAYBEL_4:40 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "L")) ($#k1_waybel_4 :::"-waybelow"::: ) ")" ) ($#k5_waybel_4 :::"-below"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel_3 :::"waybelow"::: ) (Set (Var "x")))))) ; theorem :: WAYBEL_4:41 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool (Set ($#k2_waybel_4 :::"IntRel"::: ) (Set (Var "L"))) "is" ($#v6_waybel_4 :::"approximating"::: ) )) ; registrationlet "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::); cluster (Set "L" ($#k1_waybel_4 :::"-waybelow"::: ) ) -> ($#v6_waybel_4 :::"approximating"::: ) ; end; registrationlet "L" be ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v5_waybel_4 :::"auxiliary"::: ) ($#v6_waybel_4 :::"approximating"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "L" be ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::); func :::"App"::: "L" -> ($#m1_hidden :::"set"::: ) means :: WAYBEL_4:def 19 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "a")) "is" ($#v5_waybel_4 :::"auxiliary"::: ) ($#v6_waybel_4 :::"approximating"::: ) ($#m1_subset_1 :::"Relation":::) "of" "L") ")" )); end; :: deftheorem defines :::"App"::: WAYBEL_4:def 19 : (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k12_waybel_4 :::"App"::: ) (Set (Var "L")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "a")) "is" ($#v5_waybel_4 :::"auxiliary"::: ) ($#v6_waybel_4 :::"approximating"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L"))) ")" )) ")" ))); registrationlet "L" be ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::); cluster (Set ($#k12_waybel_4 :::"App"::: ) "L") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: WAYBEL_4:42 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "mp")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set (Var "L")) ")" ) ")" ) "st" (Bool (Bool (Set (Var "mp")) "is" ($#v7_waybel_4 :::"approximating"::: ) ) & (Bool (Set (Var "mp")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k8_waybel_4 :::"MonSet"::: ) (Set (Var "L")) ")" )))) "holds" (Bool "ex" (Set (Var "AR")) "being" ($#v5_waybel_4 :::"auxiliary"::: ) ($#v6_waybel_4 :::"approximating"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "AR")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_waybel_4 :::"Map2Rel"::: ) (Set (Var "L")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "mp"))))))) ; theorem :: WAYBEL_4:43 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" (Set "(" ($#k11_waybel_4 :::"DownMap"::: ) (Set (Var "I")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) where I "is" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) : (Bool verum) "}" ) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel_3 :::"waybelow"::: ) (Set (Var "x")))))) ; theorem :: WAYBEL_4:44 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v2_waybel_2 :::"meet-continuous"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" (Set (Var "AR")) ($#k5_waybel_4 :::"-below"::: ) (Set (Var "x")) ")" ) where AR "is" ($#v5_waybel_4 :::"auxiliary"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) : (Bool (Set (Var "AR")) ($#r2_hidden :::"in"::: ) (Set ($#k12_waybel_4 :::"App"::: ) (Set (Var "L")))) "}" ) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel_3 :::"waybelow"::: ) (Set (Var "x")))))) ; theorem :: WAYBEL_4:45 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v3_waybel_3 :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "R")) "being" ($#v5_waybel_4 :::"auxiliary"::: ) ($#v6_waybel_4 :::"approximating"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Set (Var "L")) ($#k1_waybel_4 :::"-waybelow"::: ) ) ($#r1_relset_1 :::"c="::: ) (Set (Var "R"))) & (Bool (Set (Set (Var "L")) ($#k1_waybel_4 :::"-waybelow"::: ) ) "is" ($#v6_waybel_4 :::"approximating"::: ) ) ")" )) ")" )) ; theorem :: WAYBEL_4:46 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v3_waybel_3 :::"continuous"::: ) ) "iff" (Bool "(" (Bool (Set (Var "L")) "is" ($#v2_waybel_2 :::"meet-continuous"::: ) ) & (Bool "ex" (Set (Var "R")) "being" ($#v5_waybel_4 :::"auxiliary"::: ) ($#v6_waybel_4 :::"approximating"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "st" (Bool "for" (Set (Var "R9")) "being" ($#v5_waybel_4 :::"auxiliary"::: ) ($#v6_waybel_4 :::"approximating"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "R")) ($#r1_relset_1 :::"c="::: ) (Set (Var "R9"))))) ")" ) ")" )) ; definitionlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; let "AR" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "L")); attr "AR" is :::"satisfying_SI"::: means :: WAYBEL_4:def 20 (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "AR") & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "z")))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "AR") & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "AR") & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) ")" ))); end; :: deftheorem defines :::"satisfying_SI"::: WAYBEL_4:def 20 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "AR")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "AR")) "is" ($#v8_waybel_4 :::"satisfying_SI"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "AR"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "z")))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "AR"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "AR"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) ")" ))) ")" ))); definitionlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; let "AR" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "L")); attr "AR" is :::"satisfying_INT"::: means :: WAYBEL_4:def 21 (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "AR")) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "AR") & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "AR") ")" ))); end; :: deftheorem defines :::"satisfying_INT"::: WAYBEL_4:def 21 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "AR")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "AR")) "is" ($#v9_waybel_4 :::"satisfying_INT"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "AR")))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "AR"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "AR"))) ")" ))) ")" ))); theorem :: WAYBEL_4:47 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "AR")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "AR")) "is" ($#v8_waybel_4 :::"satisfying_SI"::: ) )) "holds" (Bool (Set (Var "AR")) "is" ($#v9_waybel_4 :::"satisfying_INT"::: ) ))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v8_waybel_4 :::"satisfying_SI"::: ) -> ($#v9_waybel_4 :::"satisfying_INT"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: WAYBEL_4:48 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "AR")) "being" ($#v6_waybel_4 :::"approximating"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set (Var "y"))))) "holds" (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "u")) "," (Set (Var "x")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "AR"))) & (Bool (Bool "not" (Set (Var "u")) ($#r3_orders_2 :::"<="::: ) (Set (Var "y")))) ")" ))))) ; theorem :: WAYBEL_4:49 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "R")) "being" ($#v1_waybel_4 :::"auxiliary(i)"::: ) ($#v3_waybel_4 :::"auxiliary(iii)"::: ) ($#v6_waybel_4 :::"approximating"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "z")))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set (Var "y"))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) ")" ))))) ; theorem :: WAYBEL_4:50 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "R")) "being" ($#v5_waybel_4 :::"auxiliary"::: ) ($#v6_waybel_4 :::"approximating"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "z"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "z")))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) ")" ))))) ; theorem :: WAYBEL_4:51 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool (Set (Set (Var "L")) ($#k1_waybel_4 :::"-waybelow"::: ) ) "is" ($#v8_waybel_4 :::"satisfying_SI"::: ) )) ; registrationlet "L" be ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::); cluster (Set "L" ($#k1_waybel_4 :::"-waybelow"::: ) ) -> ($#v8_waybel_4 :::"satisfying_SI"::: ) ; end; theorem :: WAYBEL_4:52 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "y")))) "holds" (Bool "ex" (Set (Var "x9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "x9"))) & (Bool (Set (Var "x9")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "y"))) ")" )))) ; theorem :: WAYBEL_4:53 (Bool "for" (Set (Var "L")) "being" ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "y"))) "iff" (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "y")) ($#r3_orders_2 :::"<="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "D"))))) "holds" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "x")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "d"))) ")" ))) ")" ))) ; begin definitionlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "L"))); pred "X" :::"is_directed_wrt"::: "R" means :: WAYBEL_4:def 22 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") ")" ))); end; :: deftheorem defines :::"is_directed_wrt"::: WAYBEL_4:def 22 : (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 "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_waybel_4 :::"is_directed_wrt"::: ) (Set (Var "R"))) "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 (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ))) ")" )))); theorem :: WAYBEL_4:54 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r1_waybel_4 :::"is_directed_wrt"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L"))))) "holds" (Bool (Set (Var "X")) "is" ($#v1_waybel_0 :::"directed"::: ) ))) ; definitionlet "X", "x" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_hidden :::"Relation":::); pred "x" :::"is_maximal_wrt"::: "X" "," "R" means :: WAYBEL_4:def 23 (Bool "(" (Bool "x" ($#r2_hidden :::"in"::: ) "X") & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "X") "or" "not" (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) "x") "or" "not" (Bool (Set ($#k4_tarski :::"["::: ) "x" "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") ")" ) ")" ) ")" ); end; :: deftheorem defines :::"is_maximal_wrt"::: WAYBEL_4:def 23 : (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_waybel_4 :::"is_maximal_wrt"::: ) (Set (Var "X")) "," (Set (Var "R"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "or" "not" (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set (Var "x"))) "or" "not" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ) ")" ) ")" ) ")" ))); definitionlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); pred "x" :::"is_maximal_in"::: "X" means :: WAYBEL_4:def 24 (Bool "x" ($#r2_waybel_4 :::"is_maximal_wrt"::: ) "X" "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "L")); end; :: deftheorem defines :::"is_maximal_in"::: WAYBEL_4:def 24 : (Bool "for" (Set (Var "L")) "being" ($#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 (Set (Var "x")) ($#r3_waybel_4 :::"is_maximal_in"::: ) (Set (Var "X"))) "iff" (Bool (Set (Var "x")) ($#r2_waybel_4 :::"is_maximal_wrt"::: ) (Set (Var "X")) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L")))) ")" )))); theorem :: WAYBEL_4:55 (Bool "for" (Set (Var "L")) "being" ($#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 (Set (Var "x")) ($#r3_waybel_4 :::"is_maximal_in"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "or" "not" (Bool (Set (Var "x")) ($#r2_orders_2 :::"<"::: ) (Set (Var "y"))) ")" ) ")" ) ")" ) ")" )))) ; definitionlet "X", "x" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_hidden :::"Relation":::); pred "x" :::"is_minimal_wrt"::: "X" "," "R" means :: WAYBEL_4:def 25 (Bool "(" (Bool "x" ($#r2_hidden :::"in"::: ) "X") & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "X") "or" "not" (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) "x") "or" "not" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," "x" ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") ")" ) ")" ) ")" ); end; :: deftheorem defines :::"is_minimal_wrt"::: WAYBEL_4:def 25 : (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r4_waybel_4 :::"is_minimal_wrt"::: ) (Set (Var "X")) "," (Set (Var "R"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "or" "not" (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set (Var "x"))) "or" "not" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ) ")" ) ")" ) ")" ))); definitionlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); pred "x" :::"is_minimal_in"::: "X" means :: WAYBEL_4:def 26 (Bool "x" ($#r4_waybel_4 :::"is_minimal_wrt"::: ) "X" "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "L")); end; :: deftheorem defines :::"is_minimal_in"::: WAYBEL_4:def 26 : (Bool "for" (Set (Var "L")) "being" ($#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 (Set (Var "x")) ($#r5_waybel_4 :::"is_minimal_in"::: ) (Set (Var "X"))) "iff" (Bool (Set (Var "x")) ($#r4_waybel_4 :::"is_minimal_wrt"::: ) (Set (Var "X")) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L")))) ")" )))); theorem :: WAYBEL_4:56 (Bool "for" (Set (Var "L")) "being" ($#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 (Set (Var "x")) ($#r5_waybel_4 :::"is_minimal_in"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "or" "not" (Bool (Set (Var "x")) ($#r2_orders_2 :::">"::: ) (Set (Var "y"))) ")" ) ")" ) ")" ) ")" )))) ; theorem :: WAYBEL_4:57 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "AR")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "AR")) "is" ($#v8_waybel_4 :::"satisfying_SI"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "y")) ($#r2_waybel_4 :::"is_maximal_wrt"::: ) (Set (Set (Var "AR")) ($#k5_waybel_4 :::"-below"::: ) (Set (Var "x"))) "," (Set (Var "AR"))))) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "AR")))))) ; theorem :: WAYBEL_4:58 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "AR")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "y")) ($#r2_waybel_4 :::"is_maximal_wrt"::: ) (Set (Set (Var "AR")) ($#k5_waybel_4 :::"-below"::: ) (Set (Var "x"))) "," (Set (Var "AR"))))) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "AR"))) ")" )) "holds" (Bool (Set (Var "AR")) "is" ($#v8_waybel_4 :::"satisfying_SI"::: ) ))) ; theorem :: WAYBEL_4:59 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "AR")) "being" ($#v2_waybel_4 :::"auxiliary(ii)"::: ) ($#v3_waybel_4 :::"auxiliary(iii)"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "AR")) "is" ($#v9_waybel_4 :::"satisfying_INT"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "AR")) ($#k5_waybel_4 :::"-below"::: ) (Set (Var "x"))) ($#r1_waybel_4 :::"is_directed_wrt"::: ) (Set (Var "AR")))))) ; theorem :: WAYBEL_4:60 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "AR")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "AR")) ($#k5_waybel_4 :::"-below"::: ) (Set (Var "x"))) ($#r1_waybel_4 :::"is_directed_wrt"::: ) (Set (Var "AR"))) ")" )) "holds" (Bool (Set (Var "AR")) "is" ($#v9_waybel_4 :::"satisfying_INT"::: ) ))) ; theorem :: WAYBEL_4:61 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "R")) "being" ($#v1_waybel_4 :::"auxiliary(i)"::: ) ($#v2_waybel_4 :::"auxiliary(ii)"::: ) ($#v3_waybel_4 :::"auxiliary(iii)"::: ) ($#v6_waybel_4 :::"approximating"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v9_waybel_4 :::"satisfying_INT"::: ) )) "holds" (Bool (Set (Var "R")) "is" ($#v8_waybel_4 :::"satisfying_SI"::: ) ))) ; registrationlet "L" be ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::); cluster ($#v5_waybel_4 :::"auxiliary"::: ) ($#v6_waybel_4 :::"approximating"::: ) ($#v9_waybel_4 :::"satisfying_INT"::: ) -> ($#v5_waybel_4 :::"auxiliary"::: ) ($#v6_waybel_4 :::"approximating"::: ) ($#v8_waybel_4 :::"satisfying_SI"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") ($#k2_zfmisc_1 :::":]"::: ) )); end;