:: WAYBEL_0 semantic presentation begin definitionlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); attr "X" is :::"directed"::: means :: WAYBEL_0:def 1 (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 (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "z"))) & (Bool (Set (Var "y")) ($#r1_orders_2 :::"<="::: ) (Set (Var "z"))) ")" ))); attr "X" is :::"filtered"::: means :: WAYBEL_0:def 2 (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 (Var "z")) ($#r1_orders_2 :::"<="::: ) (Set (Var "x"))) & (Bool (Set (Var "z")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) ")" ))); end; :: deftheorem defines :::"directed"::: WAYBEL_0:def 1 : (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 "(" (Bool (Set (Var "X")) "is" ($#v1_waybel_0 :::"directed"::: ) ) "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 (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "z"))) & (Bool (Set (Var "y")) ($#r1_orders_2 :::"<="::: ) (Set (Var "z"))) ")" ))) ")" ))); :: deftheorem defines :::"filtered"::: WAYBEL_0:def 2 : (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 "(" (Bool (Set (Var "X")) "is" ($#v2_waybel_0 :::"filtered"::: ) ) "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 (Var "z")) ($#r1_orders_2 :::"<="::: ) (Set (Var "x"))) & (Bool (Set (Var "z")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) ")" ))) ")" ))); theorem :: WAYBEL_0:1 (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 "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "X")) "is" ($#v1_waybel_0 :::"directed"::: ) ) ")" ) "iff" (Bool "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "Y"))) ")" ))) ")" ))) ; theorem :: WAYBEL_0:2 (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 "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "X")) "is" ($#v2_waybel_0 :::"filtered"::: ) ) ")" ) "iff" (Bool "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "Y"))) ")" ))) ")" ))) ; registrationlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v1_waybel_0 :::"directed"::: ) ($#v2_waybel_0 :::"filtered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))); end; registrationlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_waybel_0 :::"directed"::: ) ($#v2_waybel_0 :::"filtered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))); end; theorem :: WAYBEL_0:3 (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 "X1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L1")) (Bool "for" (Set (Var "X2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L2")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_hidden :::"="::: ) (Set (Var "X2"))) & (Bool (Set (Var "X1")) "is" ($#v1_waybel_0 :::"directed"::: ) )) "holds" (Bool (Set (Var "X2")) "is" ($#v1_waybel_0 :::"directed"::: ) )))) ; theorem :: WAYBEL_0:4 (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 "X1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L1")) (Bool "for" (Set (Var "X2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L2")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_hidden :::"="::: ) (Set (Var "X2"))) & (Bool (Set (Var "X1")) "is" ($#v2_waybel_0 :::"filtered"::: ) )) "holds" (Bool (Set (Var "X2")) "is" ($#v2_waybel_0 :::"filtered"::: ) )))) ; theorem :: WAYBEL_0:5 (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 "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) "is" ($#v1_waybel_0 :::"directed"::: ) ) & (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) "is" ($#v2_waybel_0 :::"filtered"::: ) ) ")" ))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#v1_waybel_0 :::"directed"::: ) ($#v2_waybel_0 :::"filtered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))); end; registrationlet "L" be ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k2_struct_0 :::"[#]"::: ) "L") -> ($#v1_waybel_0 :::"directed"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k2_struct_0 :::"[#]"::: ) "L") -> ($#v1_waybel_0 :::"directed"::: ) ; end; registrationlet "L" be ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k2_struct_0 :::"[#]"::: ) "L") -> ($#v2_waybel_0 :::"filtered"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k2_struct_0 :::"[#]"::: ) "L") -> ($#v2_waybel_0 :::"filtered"::: ) ; 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 :::"filtered-infs-inheriting"::: means :: WAYBEL_0:def 3 (Bool "for" (Set (Var "X")) "being" ($#v2_waybel_0 :::"filtered"::: ) ($#m1_subset_1 :::"Subset":::) "of" "S" "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (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 :::"directed-sups-inheriting"::: means :: WAYBEL_0:def 4 (Bool "for" (Set (Var "X")) "being" ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" "S" "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (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 :::"filtered-infs-inheriting"::: WAYBEL_0:def 3 : (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" ($#v3_waybel_0 :::"filtered-infs-inheriting"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#v2_waybel_0 :::"filtered"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (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 :::"directed-sups-inheriting"::: WAYBEL_0:def 4 : (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" ($#v4_waybel_0 :::"directed-sups-inheriting"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (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"::: ) -> ($#v3_waybel_0 :::"filtered-infs-inheriting"::: ) for ($#m1_yellow_0 :::"SubRelStr"::: ) "of" "L"; cluster ($#v8_yellow_0 :::"sups-inheriting"::: ) -> ($#v4_waybel_0 :::"directed-sups-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 :: WAYBEL_0:6 (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"::: ) ($#v3_waybel_0 :::"filtered-infs-inheriting"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#v2_waybel_0 :::"filtered"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) "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 :: WAYBEL_0:7 (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"::: ) ($#v4_waybel_0 :::"directed-sups-inheriting"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) "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")) ")" )) ")" )))) ; begin definitionlet "L1", "L2" be ($#l1_orders_2 :::"RelStr"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "L1")) "," (Set (Const "L2")); attr "f" is :::"antitone"::: means :: WAYBEL_0:def 5 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L1" "st" (Bool (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y")))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "L2" "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "a")) ($#r1_orders_2 :::">="::: ) (Set (Var "b"))))); end; :: deftheorem defines :::"antitone"::: WAYBEL_0:def 5 : (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_waybel_0 :::"antitone"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) "st" (Bool (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y")))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L2")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "a")) ($#r1_orders_2 :::">="::: ) (Set (Var "b"))))) ")" ))); definitionlet "L" be ($#l1_struct_0 :::"1-sorted"::: ) ; attr "c2" is :::"strict"::: ; struct :::"NetStr"::: "over" "L" -> ($#l1_orders_2 :::"RelStr"::: ) ; aggr :::"NetStr":::(# :::"carrier":::, :::"InternalRel":::, :::"mapping"::: #) -> ($#l1_waybel_0 :::"NetStr"::: ) "over" "L"; sel :::"mapping"::: "c2" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c2") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"); end; registrationlet "L" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "O" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")); let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "L"))); cluster (Set ($#g1_waybel_0 :::"NetStr"::: ) "(#" "X" "," "O" "," "F" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; definitionlet "N" be ($#l1_orders_2 :::"RelStr"::: ) ; attr "N" is :::"directed"::: means :: WAYBEL_0:def 6 (Bool (Set ($#k2_struct_0 :::"[#]"::: ) "N") "is" ($#v1_waybel_0 :::"directed"::: ) ); end; :: deftheorem defines :::"directed"::: WAYBEL_0:def 6 : (Bool "for" (Set (Var "N")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "N")) "is" ($#v7_waybel_0 :::"directed"::: ) ) "iff" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "N"))) "is" ($#v1_waybel_0 :::"directed"::: ) ) ")" )); registrationlet "L" be ($#l1_struct_0 :::"1-sorted"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v6_waybel_0 :::"strict"::: ) ($#v7_waybel_0 :::"directed"::: ) for ($#l1_waybel_0 :::"NetStr"::: ) "over" "L"; end; definitionlet "L" be ($#l1_struct_0 :::"1-sorted"::: ) ; mode prenet of "L" is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_waybel_0 :::"directed"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" "L"; end; definitionlet "L" be ($#l1_struct_0 :::"1-sorted"::: ) ; mode net of "L" is ($#v4_orders_2 :::"transitive"::: ) ($#l1_waybel_0 :::"prenet":::) "of" "L"; end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "N" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Const "L")); func :::"netmap"::: "(" "N" "," "L" ")" -> ($#m1_subset_1 :::"Function":::) "of" "N" "," "L" equals :: WAYBEL_0:def 7 (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" "N"); let "i" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "N")); func "N" :::"."::: "i" -> ($#m1_subset_1 :::"Element":::) "of" "L" equals :: WAYBEL_0:def 8 (Set (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" "N") ($#k3_funct_2 :::"."::: ) "i"); end; :: deftheorem defines :::"netmap"::: WAYBEL_0:def 7 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L")) "holds" (Bool (Set ($#k1_waybel_0 :::"netmap"::: ) "(" (Set (Var "N")) "," (Set (Var "L")) ")" ) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N")))))); :: deftheorem defines :::"."::: WAYBEL_0:def 8 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "holds" (Bool (Set (Set (Var "N")) ($#k2_waybel_0 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N"))) ($#k3_funct_2 :::"."::: ) (Set (Var "i"))))))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "N" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Const "L")); attr "N" is :::"monotone"::: means :: WAYBEL_0:def 9 (Bool (Set ($#k1_waybel_0 :::"netmap"::: ) "(" "N" "," "L" ")" ) "is" ($#v5_orders_3 :::"monotone"::: ) ); attr "N" is :::"antitone"::: means :: WAYBEL_0:def 10 (Bool (Set ($#k1_waybel_0 :::"netmap"::: ) "(" "N" "," "L" ")" ) "is" ($#v5_waybel_0 :::"antitone"::: ) ); end; :: deftheorem defines :::"monotone"::: WAYBEL_0:def 9 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "N")) "is" ($#v8_waybel_0 :::"monotone"::: ) ) "iff" (Bool (Set ($#k1_waybel_0 :::"netmap"::: ) "(" (Set (Var "N")) "," (Set (Var "L")) ")" ) "is" ($#v5_orders_3 :::"monotone"::: ) ) ")" ))); :: deftheorem defines :::"antitone"::: WAYBEL_0:def 10 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "N")) "is" ($#v9_waybel_0 :::"antitone"::: ) ) "iff" (Bool (Set ($#k1_waybel_0 :::"netmap"::: ) "(" (Set (Var "N")) "," (Set (Var "L")) ")" ) "is" ($#v5_waybel_0 :::"antitone"::: ) ) ")" ))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "N" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Const "L")); let "X" be ($#m1_hidden :::"set"::: ) ; pred "N" :::"is_eventually_in"::: "X" means :: WAYBEL_0:def 11 (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" "N" "st" (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" "N" "st" (Bool (Bool (Set (Var "i")) ($#r1_orders_2 :::"<="::: ) (Set (Var "j")))) "holds" (Bool (Set "N" ($#k2_waybel_0 :::"."::: ) (Set (Var "j"))) ($#r2_hidden :::"in"::: ) "X"))); pred "N" :::"is_often_in"::: "X" means :: WAYBEL_0:def 12 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" "N" (Bool "ex" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" "N" "st" (Bool "(" (Bool (Set (Var "i")) ($#r1_orders_2 :::"<="::: ) (Set (Var "j"))) & (Bool (Set "N" ($#k2_waybel_0 :::"."::: ) (Set (Var "j"))) ($#r2_hidden :::"in"::: ) "X") ")" ))); end; :: deftheorem defines :::"is_eventually_in"::: WAYBEL_0:def 11 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "N")) ($#r1_waybel_0 :::"is_eventually_in"::: ) (Set (Var "X"))) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "st" (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "st" (Bool (Bool (Set (Var "i")) ($#r1_orders_2 :::"<="::: ) (Set (Var "j")))) "holds" (Bool (Set (Set (Var "N")) ($#k2_waybel_0 :::"."::: ) (Set (Var "j"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) ")" )))); :: deftheorem defines :::"is_often_in"::: WAYBEL_0:def 12 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "N")) ($#r2_waybel_0 :::"is_often_in"::: ) (Set (Var "X"))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) (Bool "ex" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "st" (Bool "(" (Bool (Set (Var "i")) ($#r1_orders_2 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Set (Var "N")) ($#k2_waybel_0 :::"."::: ) (Set (Var "j"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ))) ")" )))); theorem :: WAYBEL_0:8 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L")) (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 "(" "(" (Bool (Bool (Set (Var "N")) ($#r1_waybel_0 :::"is_eventually_in"::: ) (Set (Var "X")))) "implies" (Bool (Set (Var "N")) ($#r1_waybel_0 :::"is_eventually_in"::: ) (Set (Var "Y"))) ")" & "(" (Bool (Bool (Set (Var "N")) ($#r2_waybel_0 :::"is_often_in"::: ) (Set (Var "X")))) "implies" (Bool (Set (Var "N")) ($#r2_waybel_0 :::"is_often_in"::: ) (Set (Var "Y"))) ")" ")" )))) ; theorem :: WAYBEL_0:9 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "N")) ($#r1_waybel_0 :::"is_eventually_in"::: ) (Set (Var "X"))) "iff" (Bool (Bool "not" (Set (Var "N")) ($#r2_waybel_0 :::"is_often_in"::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#k6_subset_1 :::"\"::: ) (Set (Var "X"))))) ")" )))) ; theorem :: WAYBEL_0:10 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "N")) ($#r2_waybel_0 :::"is_often_in"::: ) (Set (Var "X"))) "iff" (Bool (Bool "not" (Set (Var "N")) ($#r1_waybel_0 :::"is_eventually_in"::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ($#k6_subset_1 :::"\"::: ) (Set (Var "X"))))) ")" )))) ; scheme :: WAYBEL_0:sch 1 HoldsEventually{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) , F2() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set F1 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "(" (Bool (Set F2 "(" ")" ) ($#r1_waybel_0 :::"is_eventually_in"::: ) "{" (Set "(" (Set F2 "(" ")" ) ($#k2_waybel_0 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m1_subset_1 :::"Element":::) "of" (Set F2 "(" ")" ) : (Bool P1[(Set (Set F2 "(" ")" ) ($#k2_waybel_0 :::"."::: ) (Set (Var "k")))]) "}" ) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set F2 "(" ")" ) "st" (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set F2 "(" ")" ) "st" (Bool (Bool (Set (Var "i")) ($#r1_orders_2 :::"<="::: ) (Set (Var "j")))) "holds" (Bool P1[(Set (Set F2 "(" ")" ) ($#k2_waybel_0 :::"."::: ) (Set (Var "j")))]))) ")" ) proof end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "N" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Const "L")); attr "N" is :::"eventually-directed"::: means :: WAYBEL_0:def 13 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" "N" "holds" (Bool "N" ($#r1_waybel_0 :::"is_eventually_in"::: ) "{" (Set "(" "N" ($#k2_waybel_0 :::"."::: ) (Set (Var "j")) ")" ) where j "is" ($#m1_subset_1 :::"Element":::) "of" "N" : (Bool (Set "N" ($#k2_waybel_0 :::"."::: ) (Set (Var "i"))) ($#r1_orders_2 :::"<="::: ) (Set "N" ($#k2_waybel_0 :::"."::: ) (Set (Var "j")))) "}" )); attr "N" is :::"eventually-filtered"::: means :: WAYBEL_0:def 14 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" "N" "holds" (Bool "N" ($#r1_waybel_0 :::"is_eventually_in"::: ) "{" (Set "(" "N" ($#k2_waybel_0 :::"."::: ) (Set (Var "j")) ")" ) where j "is" ($#m1_subset_1 :::"Element":::) "of" "N" : (Bool (Set "N" ($#k2_waybel_0 :::"."::: ) (Set (Var "i"))) ($#r1_orders_2 :::">="::: ) (Set "N" ($#k2_waybel_0 :::"."::: ) (Set (Var "j")))) "}" )); end; :: deftheorem defines :::"eventually-directed"::: WAYBEL_0:def 13 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "N")) "is" ($#v10_waybel_0 :::"eventually-directed"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "holds" (Bool (Set (Var "N")) ($#r1_waybel_0 :::"is_eventually_in"::: ) "{" (Set "(" (Set (Var "N")) ($#k2_waybel_0 :::"."::: ) (Set (Var "j")) ")" ) where j "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) : (Bool (Set (Set (Var "N")) ($#k2_waybel_0 :::"."::: ) (Set (Var "i"))) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "N")) ($#k2_waybel_0 :::"."::: ) (Set (Var "j")))) "}" )) ")" ))); :: deftheorem defines :::"eventually-filtered"::: WAYBEL_0:def 14 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "N")) "is" ($#v11_waybel_0 :::"eventually-filtered"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "holds" (Bool (Set (Var "N")) ($#r1_waybel_0 :::"is_eventually_in"::: ) "{" (Set "(" (Set (Var "N")) ($#k2_waybel_0 :::"."::: ) (Set (Var "j")) ")" ) where j "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) : (Bool (Set (Set (Var "N")) ($#k2_waybel_0 :::"."::: ) (Set (Var "i"))) ($#r1_orders_2 :::">="::: ) (Set (Set (Var "N")) ($#k2_waybel_0 :::"."::: ) (Set (Var "j")))) "}" )) ")" ))); theorem :: WAYBEL_0:11 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "N")) "is" ($#v10_waybel_0 :::"eventually-directed"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) (Bool "ex" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "st" (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "st" (Bool (Bool (Set (Var "j")) ($#r1_orders_2 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set (Set (Var "N")) ($#k2_waybel_0 :::"."::: ) (Set (Var "i"))) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "N")) ($#k2_waybel_0 :::"."::: ) (Set (Var "k"))))))) ")" ))) ; theorem :: WAYBEL_0:12 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "N")) "is" ($#v11_waybel_0 :::"eventually-filtered"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) (Bool "ex" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "st" (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "st" (Bool (Bool (Set (Var "j")) ($#r1_orders_2 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set (Set (Var "N")) ($#k2_waybel_0 :::"."::: ) (Set (Var "i"))) ($#r1_orders_2 :::">="::: ) (Set (Set (Var "N")) ($#k2_waybel_0 :::"."::: ) (Set (Var "k"))))))) ")" ))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_waybel_0 :::"directed"::: ) ($#v8_waybel_0 :::"monotone"::: ) -> ($#v10_waybel_0 :::"eventually-directed"::: ) for ($#l1_waybel_0 :::"NetStr"::: ) "over" "L"; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_waybel_0 :::"directed"::: ) ($#v9_waybel_0 :::"antitone"::: ) -> ($#v11_waybel_0 :::"eventually-filtered"::: ) for ($#l1_waybel_0 :::"NetStr"::: ) "over" "L"; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_waybel_0 :::"strict"::: ) ($#v7_waybel_0 :::"directed"::: ) ($#v8_waybel_0 :::"monotone"::: ) ($#v9_waybel_0 :::"antitone"::: ) for ($#l1_waybel_0 :::"NetStr"::: ) "over" "L"; end; begin definitionlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); func :::"downarrow"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" "L" means :: WAYBEL_0:def 15 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool "(" (Bool (Set (Var "y")) ($#r1_orders_2 :::">="::: ) (Set (Var "x"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "X") ")" )) ")" )); func :::"uparrow"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" "L" means :: WAYBEL_0:def 16 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool "(" (Bool (Set (Var "y")) ($#r1_orders_2 :::"<="::: ) (Set (Var "x"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "X") ")" )) ")" )); end; :: deftheorem defines :::"downarrow"::: WAYBEL_0:def 15 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "y")) ($#r1_orders_2 :::">="::: ) (Set (Var "x"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) ")" )) ")" ))); :: deftheorem defines :::"uparrow"::: WAYBEL_0:def 16 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "y")) ($#r1_orders_2 :::"<="::: ) (Set (Var "x"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) ")" )) ")" ))); theorem :: WAYBEL_0:13 (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_subset_1 :::"Subset":::) "of" (Set (Var "L1")) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L2")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y")))) "holds" (Bool "(" (Bool (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "Y")))) & (Bool (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "Y")))) ")" )))) ; theorem :: WAYBEL_0:14 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) "}" ))) ; theorem :: WAYBEL_0:15 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_orders_2 :::">="::: ) (Set (Var "y"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) "}" ))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set ($#k3_waybel_0 :::"downarrow"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k4_waybel_0 :::"uparrow"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: WAYBEL_0:16 (Bool "for" (Set (Var "L")) "being" ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "X")))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "X")))) ")" ))) ; 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")); func :::"downarrow"::: "x" -> ($#m1_subset_1 :::"Subset":::) "of" "L" equals :: WAYBEL_0:def 17 (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set ($#k6_domain_1 :::"{"::: ) "x" ($#k6_domain_1 :::"}"::: ) )); func :::"uparrow"::: "x" -> ($#m1_subset_1 :::"Subset":::) "of" "L" equals :: WAYBEL_0:def 18 (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set ($#k6_domain_1 :::"{"::: ) "x" ($#k6_domain_1 :::"}"::: ) )); end; :: deftheorem defines :::"downarrow"::: WAYBEL_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 "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))))); :: deftheorem defines :::"uparrow"::: WAYBEL_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 "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))))); theorem :: WAYBEL_0:17 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x")))) "iff" (Bool (Set (Var "y")) ($#r1_orders_2 :::"<="::: ) (Set (Var "x"))) ")" ))) ; theorem :: WAYBEL_0:18 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x")))) "iff" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) ")" ))) ; theorem :: WAYBEL_0:19 (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 "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: WAYBEL_0:20 (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 "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: WAYBEL_0:21 (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 "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 (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "y")))))) ; theorem :: WAYBEL_0:22 (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 "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 (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "y"))) ($#r1_tarski :::"c="::: ) (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x")))))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); cluster (Set ($#k5_waybel_0 :::"downarrow"::: ) "x") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ; cluster (Set ($#k6_waybel_0 :::"uparrow"::: ) "x") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_waybel_0 :::"filtered"::: ) ; end; definitionlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); attr "X" is :::"lower"::: means :: WAYBEL_0:def 19 (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")) ($#r1_orders_2 :::"<="::: ) (Set (Var "x")))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "X")); attr "X" is :::"upper"::: means :: WAYBEL_0:def 20 (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 "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "X")); end; :: deftheorem defines :::"lower"::: WAYBEL_0:def 19 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v12_waybel_0 :::"lower"::: ) ) "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")) ($#r1_orders_2 :::"<="::: ) (Set (Var "x")))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) ")" ))); :: deftheorem defines :::"upper"::: WAYBEL_0:def 20 : (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 "(" (Bool (Set (Var "X")) "is" ($#v13_waybel_0 :::"upper"::: ) ) "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 "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) ")" ))); registrationlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v12_waybel_0 :::"lower"::: ) ($#v13_waybel_0 :::"upper"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))); end; theorem :: WAYBEL_0:23 (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 "(" (Bool (Set (Var "X")) "is" ($#v12_waybel_0 :::"lower"::: ) ) "iff" (Bool (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) ")" ))) ; theorem :: WAYBEL_0:24 (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 "(" (Bool (Set (Var "X")) "is" ($#v13_waybel_0 :::"upper"::: ) ) "iff" (Bool (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) ")" ))) ; theorem :: WAYBEL_0:25 (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 "X1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L1")) (Bool "for" (Set (Var "X2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L2")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_hidden :::"="::: ) (Set (Var "X2")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "X1")) "is" ($#v12_waybel_0 :::"lower"::: ) )) "implies" (Bool (Set (Var "X2")) "is" ($#v12_waybel_0 :::"lower"::: ) ) ")" & "(" (Bool (Bool (Set (Var "X1")) "is" ($#v13_waybel_0 :::"upper"::: ) )) "implies" (Bool (Set (Var "X2")) "is" ($#v13_waybel_0 :::"upper"::: ) ) ")" ")" )))) ; theorem :: WAYBEL_0:26 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "X")) "is" ($#v12_waybel_0 :::"lower"::: ) ) ")" )) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "A"))) "is" ($#v12_waybel_0 :::"lower"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L"))))) ; theorem :: WAYBEL_0:27 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v12_waybel_0 :::"lower"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v12_waybel_0 :::"lower"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Y"))) "is" ($#v12_waybel_0 :::"lower"::: ) ) & (Bool (Set (Set (Var "X")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Y"))) "is" ($#v12_waybel_0 :::"lower"::: ) ) ")" ))) ; theorem :: WAYBEL_0:28 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "X")) "is" ($#v13_waybel_0 :::"upper"::: ) ) ")" )) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "A"))) "is" ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L"))))) ; theorem :: WAYBEL_0:29 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v13_waybel_0 :::"upper"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v13_waybel_0 :::"upper"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Y"))) "is" ($#v13_waybel_0 :::"upper"::: ) ) & (Bool (Set (Set (Var "X")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Y"))) "is" ($#v13_waybel_0 :::"upper"::: ) ) ")" ))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set ($#k3_waybel_0 :::"downarrow"::: ) "X") -> ($#v12_waybel_0 :::"lower"::: ) ; cluster (Set ($#k4_waybel_0 :::"uparrow"::: ) "X") -> ($#v13_waybel_0 :::"upper"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); cluster (Set ($#k5_waybel_0 :::"downarrow"::: ) "x") -> ($#v12_waybel_0 :::"lower"::: ) ; cluster (Set ($#k6_waybel_0 :::"uparrow"::: ) "x") -> ($#v13_waybel_0 :::"upper"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k2_struct_0 :::"[#]"::: ) "L") -> ($#v12_waybel_0 :::"lower"::: ) ($#v13_waybel_0 :::"upper"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v12_waybel_0 :::"lower"::: ) ($#v13_waybel_0 :::"upper"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))); 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 ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#v12_waybel_0 :::"lower"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_waybel_0 :::"filtered"::: ) ($#v13_waybel_0 :::"upper"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))); end; registrationlet "L" be ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"Poset":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#v2_waybel_0 :::"filtered"::: ) ($#v12_waybel_0 :::"lower"::: ) ($#v13_waybel_0 :::"upper"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))); end; theorem :: WAYBEL_0:30 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_waybel_0 :::"directed"::: ) ) "iff" (Bool (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "X"))) "is" ($#v1_waybel_0 :::"directed"::: ) ) ")" ))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set ($#k3_waybel_0 :::"downarrow"::: ) "X") -> ($#v1_waybel_0 :::"directed"::: ) ; end; theorem :: WAYBEL_0:31 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X"))) "iff" (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "X")))) ")" )))) ; theorem :: WAYBEL_0:32 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) "iff" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "X"))) "," (Set (Var "L"))) ")" ))) ; theorem :: WAYBEL_0:33 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "X")) ")" ))))) ; theorem :: WAYBEL_0:34 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x"))) "," (Set (Var "L"))) & (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ))) ; theorem :: WAYBEL_0:35 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v2_waybel_0 :::"filtered"::: ) ) "iff" (Bool (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "X"))) "is" ($#v2_waybel_0 :::"filtered"::: ) ) ")" ))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#v2_waybel_0 :::"filtered"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set ($#k4_waybel_0 :::"uparrow"::: ) "X") -> ($#v2_waybel_0 :::"filtered"::: ) ; end; theorem :: WAYBEL_0:36 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X"))) "iff" (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "X")))) ")" )))) ; theorem :: WAYBEL_0:37 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) "iff" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "X"))) "," (Set (Var "L"))) ")" ))) ; theorem :: WAYBEL_0:38 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) "holds" (Bool (Set ($#k2_yellow_0 :::"inf"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::"inf"::: ) (Set "(" ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "X")) ")" ))))) ; theorem :: WAYBEL_0:39 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x"))) "," (Set (Var "L"))) & (Bool (Set ($#k2_yellow_0 :::"inf"::: ) (Set "(" ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ))) ; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; mode Ideal of "L" is ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#v12_waybel_0 :::"lower"::: ) ($#m1_subset_1 :::"Subset":::) "of" "L"; mode Filter of "L" is ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_waybel_0 :::"filtered"::: ) ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" "L"; end; theorem :: WAYBEL_0:40 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#v12_waybel_0 :::"lower"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_waybel_0 :::"directed"::: ) ) "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 (Set (Set (Var "x")) ($#k13_lattice3 :::""\/""::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) ")" ))) ; theorem :: WAYBEL_0:41 (Bool "for" (Set (Var "L")) "being" ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v2_waybel_0 :::"filtered"::: ) ) "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 (Set (Set (Var "x")) ($#k12_lattice3 :::""/\""::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) ")" ))) ; theorem :: WAYBEL_0:42 (Bool "for" (Set (Var "L")) "being" ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v12_waybel_0 :::"lower"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_waybel_0 :::"directed"::: ) ) "iff" (Bool "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) ")" ))) ; theorem :: WAYBEL_0:43 (Bool "for" (Set (Var "L")) "being" ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v2_waybel_0 :::"filtered"::: ) ) "iff" (Bool "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) ")" ))) ; theorem :: WAYBEL_0:44 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_lattice3 :::"with_suprema"::: ) ) "or" (Bool (Set (Var "L")) "is" ($#v2_lattice3 :::"with_infima"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v12_waybel_0 :::"lower"::: ) ) & (Bool (Set (Var "X")) "is" ($#v1_waybel_0 :::"directed"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v12_waybel_0 :::"lower"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_waybel_0 :::"directed"::: ) )) "holds" (Bool (Set (Set (Var "X")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Y"))) "is" ($#v1_waybel_0 :::"directed"::: ) ))) ; theorem :: WAYBEL_0:45 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool "(" (Bool (Set (Var "L")) "is" ($#v1_lattice3 :::"with_suprema"::: ) ) "or" (Bool (Set (Var "L")) "is" ($#v2_lattice3 :::"with_infima"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v13_waybel_0 :::"upper"::: ) ) & (Bool (Set (Var "X")) "is" ($#v2_waybel_0 :::"filtered"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v13_waybel_0 :::"upper"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v2_waybel_0 :::"filtered"::: ) )) "holds" (Bool (Set (Set (Var "X")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Y"))) "is" ($#v2_waybel_0 :::"filtered"::: ) ))) ; theorem :: WAYBEL_0:46 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "X")) "is" ($#v1_waybel_0 :::"directed"::: ) ) ")" ) & (Bool "(" "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Set (Var "X")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Y"))) ($#r1_tarski :::"c="::: ) (Set (Var "Z"))) ")" )) ")" )) "holds" (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "X")) "is" ($#v1_waybel_0 :::"directed"::: ) )))) ; theorem :: WAYBEL_0:47 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "X")) "is" ($#v2_waybel_0 :::"filtered"::: ) ) ")" ) & (Bool "(" "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Set (Var "X")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Y"))) ($#r1_tarski :::"c="::: ) (Set (Var "Z"))) ")" )) ")" )) "holds" (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "X")) "is" ($#v2_waybel_0 :::"filtered"::: ) )))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "I" be ($#m1_subset_1 :::"Ideal":::) "of" (Set (Const "L")); attr "I" is :::"principal"::: means :: WAYBEL_0:def 21 (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "I") & (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) "I") ")" )); end; :: deftheorem defines :::"principal"::: WAYBEL_0:def 21 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v14_waybel_0 :::"principal"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "I"))) ")" )) ")" ))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "F" be ($#m1_subset_1 :::"Filter":::) "of" (Set (Const "L")); attr "F" is :::"principal"::: means :: WAYBEL_0:def 22 (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "F") & (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) "F") ")" )); end; :: deftheorem defines :::"principal"::: WAYBEL_0:def 22 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v15_waybel_0 :::"principal"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "F"))) ")" )) ")" ))); theorem :: WAYBEL_0:48 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v14_waybel_0 :::"principal"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x"))))) ")" ))) ; theorem :: WAYBEL_0:49 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v15_waybel_0 :::"principal"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x"))))) ")" ))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; func :::"Ids"::: "L" -> ($#m1_hidden :::"set"::: ) equals :: WAYBEL_0:def 23 "{" (Set (Var "X")) where X "is" ($#m1_subset_1 :::"Ideal":::) "of" "L" : (Bool verum) "}" ; func :::"Filt"::: "L" -> ($#m1_hidden :::"set"::: ) equals :: WAYBEL_0:def 24 "{" (Set (Var "X")) where X "is" ($#m1_subset_1 :::"Filter":::) "of" "L" : (Bool verum) "}" ; end; :: deftheorem defines :::"Ids"::: WAYBEL_0:def 23 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k7_waybel_0 :::"Ids"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "X")) where X "is" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) : (Bool verum) "}" )); :: deftheorem defines :::"Filt"::: WAYBEL_0:def 24 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k8_waybel_0 :::"Filt"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "X")) where X "is" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) : (Bool verum) "}" )); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; func :::"Ids_0"::: "L" -> ($#m1_hidden :::"set"::: ) equals :: WAYBEL_0:def 25 (Set (Set "(" ($#k7_waybel_0 :::"Ids"::: ) "L" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )); func :::"Filt_0"::: "L" -> ($#m1_hidden :::"set"::: ) equals :: WAYBEL_0:def 26 (Set (Set "(" ($#k8_waybel_0 :::"Filt"::: ) "L" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )); end; :: deftheorem defines :::"Ids_0"::: WAYBEL_0:def 25 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k9_waybel_0 :::"Ids_0"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_waybel_0 :::"Ids"::: ) (Set (Var "L")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )))); :: deftheorem defines :::"Filt_0"::: WAYBEL_0:def 26 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k10_waybel_0 :::"Filt_0"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_waybel_0 :::"Filt"::: ) (Set (Var "L")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); func :::"finsups"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" "L" equals :: WAYBEL_0:def 27 "{" (Set "(" ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "Y")) "," "L" ")" ")" ) where Y "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "X" : (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "Y")) "," "L") "}" ; func :::"fininfs"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" "L" equals :: WAYBEL_0:def 28 "{" (Set "(" ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "Y")) "," "L" ")" ")" ) where Y "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "X" : (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "Y")) "," "L") "}" ; end; :: deftheorem defines :::"finsups"::: WAYBEL_0:def 27 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k11_waybel_0 :::"finsups"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" ")" ) where Y "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "Y")) "," (Set (Var "L"))) "}" ))); :: deftheorem defines :::"fininfs"::: WAYBEL_0:def 28 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k12_waybel_0 :::"fininfs"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" ")" ) where Y "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "Y")) "," (Set (Var "L"))) "}" ))); registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set ($#k11_waybel_0 :::"finsups"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_yellow_0 :::"upper-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set ($#k12_waybel_0 :::"fininfs"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set ($#k11_waybel_0 :::"finsups"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k12_waybel_0 :::"fininfs"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: WAYBEL_0:50 (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 "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k11_waybel_0 :::"finsups"::: ) (Set (Var "X")))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k12_waybel_0 :::"fininfs"::: ) (Set (Var "X")))) ")" ))) ; theorem :: WAYBEL_0:51 (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 "X")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "Y")) "," (Set (Var "L"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "Y")) "," (Set (Var "L"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" )) ")" )) ")" ) & (Bool "(" "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" )) "holds" (Bool (Set (Var "F")) "is" ($#v1_waybel_0 :::"directed"::: ) ))) ; registrationlet "L" be ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"Poset":::); let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set ($#k11_waybel_0 :::"finsups"::: ) "X") -> ($#v1_waybel_0 :::"directed"::: ) ; end; theorem :: WAYBEL_0:52 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "Y")) "," (Set (Var "L"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "Y")) "," (Set (Var "L"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" )) ")" )) ")" ) & (Bool "(" "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" )) "holds" (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 "F"))) ")" )))) ; theorem :: WAYBEL_0:53 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "Y")) "," (Set (Var "L"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "Y")) "," (Set (Var "L"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" )) ")" )) ")" ) & (Bool "(" "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" )) "holds" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) "iff" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "F")) "," (Set (Var "L"))) ")" ))) ; theorem :: WAYBEL_0:54 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "Y")) "," (Set (Var "L"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "Y")) "," (Set (Var "L"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" )) ")" )) ")" ) & (Bool "(" "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" ) & (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "X")))))) ; theorem :: WAYBEL_0:55 (Bool "for" (Set (Var "L")) "being" ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) "or" (Bool (Set (Var "L")) "is" ($#v3_lattice3 :::"complete"::: ) ) ")" )) "holds" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" ($#k11_waybel_0 :::"finsups"::: ) (Set (Var "X")) ")" ))))) ; theorem :: WAYBEL_0:56 (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 "X")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "Y")) "," (Set (Var "L"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "Y")) "," (Set (Var "L"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" )) ")" )) ")" ) & (Bool "(" "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" )) "holds" (Bool (Set (Var "F")) "is" ($#v2_waybel_0 :::"filtered"::: ) ))) ; registrationlet "L" be ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"Poset":::); let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); cluster (Set ($#k12_waybel_0 :::"fininfs"::: ) "X") -> ($#v2_waybel_0 :::"filtered"::: ) ; end; theorem :: WAYBEL_0:57 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "Y")) "," (Set (Var "L"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "Y")) "," (Set (Var "L"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" )) ")" )) ")" ) & (Bool "(" "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" )) "holds" (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 "F"))) ")" )))) ; theorem :: WAYBEL_0:58 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "Y")) "," (Set (Var "L"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "Y")) "," (Set (Var "L"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" )) ")" )) ")" ) & (Bool "(" "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" )) "holds" (Bool "(" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) "iff" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "F")) "," (Set (Var "L"))) ")" ))) ; theorem :: WAYBEL_0:59 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "Y")) "," (Set (Var "L"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "Y")) "," (Set (Var "L"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" )) ")" )) ")" ) & (Bool "(" "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" ) & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) "holds" (Bool (Set ($#k2_yellow_0 :::"inf"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::"inf"::: ) (Set (Var "X")))))) ; theorem :: WAYBEL_0:60 (Bool "for" (Set (Var "L")) "being" ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool "(" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L"))) "or" (Bool (Set (Var "L")) "is" ($#v3_lattice3 :::"complete"::: ) ) ")" )) "holds" (Bool (Set ($#k2_yellow_0 :::"inf"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k2_yellow_0 :::"inf"::: ) (Set "(" ($#k12_waybel_0 :::"fininfs"::: ) (Set (Var "X")) ")" ))))) ; theorem :: WAYBEL_0:61 (Bool "for" (Set (Var "L")) "being" ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set "(" ($#k11_waybel_0 :::"finsups"::: ) (Set (Var "X")) ")" ))) & (Bool "(" "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "I")))) "holds" (Bool (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set "(" ($#k11_waybel_0 :::"finsups"::: ) (Set (Var "X")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "I"))) ")" ) ")" ))) ; theorem :: WAYBEL_0:62 (Bool "for" (Set (Var "L")) "being" ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set "(" ($#k12_waybel_0 :::"fininfs"::: ) (Set (Var "X")) ")" ))) & (Bool "(" "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set "(" ($#k12_waybel_0 :::"fininfs"::: ) (Set (Var "X")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "F"))) ")" ) ")" ))) ; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; attr "L" is :::"connected"::: means :: WAYBEL_0:def 29 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) "or" (Bool (Set (Var "y")) ($#r1_orders_2 :::"<="::: ) (Set (Var "x"))) ")" )); end; :: deftheorem defines :::"connected"::: WAYBEL_0:def 29 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v16_waybel_0 :::"connected"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) "or" (Bool (Set (Var "y")) ($#r1_orders_2 :::"<="::: ) (Set (Var "x"))) ")" )) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_struct_0 :::"trivial"::: ) ($#v3_orders_2 :::"reflexive"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v16_waybel_0 :::"connected"::: ) 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"::: ) ($#v16_waybel_0 :::"connected"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; definitionmode Chain is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::); end; registrationlet "L" be ($#l1_orders_2 :::"Chain":::); cluster (Set "L" ($#k7_lattice3 :::"~"::: ) ) -> ($#v16_waybel_0 :::"connected"::: ) ; end; begin definitionmode Semilattice is ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"Poset":::); mode sup-Semilattice is ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"Poset":::); mode LATTICE is ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"Poset":::); end; theorem :: WAYBEL_0:63 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v13_waybel_0 :::"upper"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "L"))) "iff" (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "X"))) "is" ($#v5_yellow_0 :::"meet-inheriting"::: ) ) ")" ))) ; theorem :: WAYBEL_0:64 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v12_waybel_0 :::"lower"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "L"))) "iff" (Bool (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "X"))) "is" ($#v6_yellow_0 :::"join-inheriting"::: ) ) ")" ))) ; begin definitionlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "S")); pred "f" :::"preserves_inf_of"::: "X" means :: WAYBEL_0:def 30 "(" (Bool (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) "X" "," "S")) "implies" (Bool "(" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set "f" ($#k7_relset_1 :::".:"::: ) "X") "," "T") & (Bool (Set ($#k2_yellow_0 :::"inf"::: ) (Set "(" "f" ($#k7_relset_1 :::".:"::: ) "X" ")" )) ($#r1_hidden :::"="::: ) (Set "f" ($#k3_funct_2 :::"."::: ) (Set "(" ($#k2_yellow_0 :::"inf"::: ) "X" ")" ))) ")" ) ")" ; pred "f" :::"preserves_sup_of"::: "X" means :: WAYBEL_0:def 31 "(" (Bool (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) "X" "," "S")) "implies" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set "f" ($#k7_relset_1 :::".:"::: ) "X") "," "T") & (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" "f" ($#k7_relset_1 :::".:"::: ) "X" ")" )) ($#r1_hidden :::"="::: ) (Set "f" ($#k3_funct_2 :::"."::: ) (Set "(" ($#k1_yellow_0 :::"sup"::: ) "X" ")" ))) ")" ) ")" ; end; :: deftheorem defines :::"preserves_inf_of"::: WAYBEL_0:def 30 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r3_waybel_0 :::"preserves_inf_of"::: ) (Set (Var "X"))) "iff" "(" (Bool (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "S")))) "implies" (Bool "(" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X"))) "," (Set (Var "T"))) & (Bool (Set ($#k2_yellow_0 :::"inf"::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k2_yellow_0 :::"inf"::: ) (Set (Var "X")) ")" ))) ")" ) ")" ")" )))); :: deftheorem defines :::"preserves_sup_of"::: WAYBEL_0:def 31 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r4_waybel_0 :::"preserves_sup_of"::: ) (Set (Var "X"))) "iff" "(" (Bool (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "S")))) "implies" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X"))) "," (Set (Var "T"))) & (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k1_yellow_0 :::"sup"::: ) (Set (Var "X")) ")" ))) ")" ) ")" ")" )))); theorem :: WAYBEL_0:65 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (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 "T1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T1"))) "#)" )) & (Bool (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"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T2"))) "#)" ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S1")) "," (Set (Var "S2")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T1")) "," (Set (Var "T2")) "st" (Bool (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set (Var "g")))) "holds" (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S1")) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T1")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "Y")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "f")) ($#r4_waybel_0 :::"preserves_sup_of"::: ) (Set (Var "X")))) "implies" (Bool (Set (Var "g")) ($#r4_waybel_0 :::"preserves_sup_of"::: ) (Set (Var "Y"))) ")" & "(" (Bool (Bool (Set (Var "f")) ($#r3_waybel_0 :::"preserves_inf_of"::: ) (Set (Var "X")))) "implies" (Bool (Set (Var "g")) ($#r3_waybel_0 :::"preserves_inf_of"::: ) (Set (Var "Y"))) ")" ")" )))))) ; definitionlet "L1", "L2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "L1")) "," (Set (Const "L2")); attr "f" is :::"infs-preserving"::: means :: WAYBEL_0:def 32 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" "L1" "holds" (Bool "f" ($#r3_waybel_0 :::"preserves_inf_of"::: ) (Set (Var "X")))); attr "f" is :::"sups-preserving"::: means :: WAYBEL_0:def 33 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" "L1" "holds" (Bool "f" ($#r4_waybel_0 :::"preserves_sup_of"::: ) (Set (Var "X")))); attr "f" is :::"meet-preserving"::: means :: WAYBEL_0:def 34 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L1" "holds" (Bool "f" ($#r3_waybel_0 :::"preserves_inf_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ))); attr "f" is :::"join-preserving"::: means :: WAYBEL_0:def 35 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L1" "holds" (Bool "f" ($#r4_waybel_0 :::"preserves_sup_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ))); attr "f" is :::"filtered-infs-preserving"::: means :: WAYBEL_0:def 36 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" "L1" "st" (Bool (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "X")) "is" ($#v2_waybel_0 :::"filtered"::: ) )) "holds" (Bool "f" ($#r3_waybel_0 :::"preserves_inf_of"::: ) (Set (Var "X")))); attr "f" is :::"directed-sups-preserving"::: means :: WAYBEL_0:def 37 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" "L1" "st" (Bool (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "X")) "is" ($#v1_waybel_0 :::"directed"::: ) )) "holds" (Bool "f" ($#r4_waybel_0 :::"preserves_sup_of"::: ) (Set (Var "X")))); end; :: deftheorem defines :::"infs-preserving"::: WAYBEL_0:def 32 : (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L1")) "holds" (Bool (Set (Var "f")) ($#r3_waybel_0 :::"preserves_inf_of"::: ) (Set (Var "X")))) ")" ))); :: deftheorem defines :::"sups-preserving"::: WAYBEL_0:def 33 : (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v18_waybel_0 :::"sups-preserving"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L1")) "holds" (Bool (Set (Var "f")) ($#r4_waybel_0 :::"preserves_sup_of"::: ) (Set (Var "X")))) ")" ))); :: deftheorem defines :::"meet-preserving"::: WAYBEL_0:def 34 : (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v19_waybel_0 :::"meet-preserving"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) "holds" (Bool (Set (Var "f")) ($#r3_waybel_0 :::"preserves_inf_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ))) ")" ))); :: deftheorem defines :::"join-preserving"::: WAYBEL_0:def 35 : (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v20_waybel_0 :::"join-preserving"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) "holds" (Bool (Set (Var "f")) ($#r4_waybel_0 :::"preserves_sup_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ))) ")" ))); :: deftheorem defines :::"filtered-infs-preserving"::: WAYBEL_0:def 36 : (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v21_waybel_0 :::"filtered-infs-preserving"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L1")) "st" (Bool (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "X")) "is" ($#v2_waybel_0 :::"filtered"::: ) )) "holds" (Bool (Set (Var "f")) ($#r3_waybel_0 :::"preserves_inf_of"::: ) (Set (Var "X")))) ")" ))); :: deftheorem defines :::"directed-sups-preserving"::: WAYBEL_0:def 37 : (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L1")) "," (Set (Var "L2")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L1")) "st" (Bool (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "X")) "is" ($#v1_waybel_0 :::"directed"::: ) )) "holds" (Bool (Set (Var "f")) ($#r4_waybel_0 :::"preserves_sup_of"::: ) (Set (Var "X")))) ")" ))); registrationlet "L1", "L2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L1") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L2")) ($#v17_waybel_0 :::"infs-preserving"::: ) -> ($#v19_waybel_0 :::"meet-preserving"::: ) ($#v21_waybel_0 :::"filtered-infs-preserving"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L1") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L2"))))); cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L1") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L2")) ($#v18_waybel_0 :::"sups-preserving"::: ) -> ($#v20_waybel_0 :::"join-preserving"::: ) ($#v22_waybel_0 :::"directed-sups-preserving"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L1") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L2"))))); end; definitionlet "S", "T" be ($#l1_orders_2 :::"RelStr"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); attr "f" is :::"isomorphic"::: means :: WAYBEL_0:def 38 (Bool "(" (Bool "f" "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool "f" "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" "T" "," "S" "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set "f" ($#k2_funct_1 :::"""::: ) )) & (Bool (Set (Var "g")) "is" ($#v5_orders_3 :::"monotone"::: ) ) ")" )) ")" ) if (Bool "(" (Bool (Bool "not" "S" "is" ($#v2_struct_0 :::"empty"::: ) )) & (Bool (Bool "not" "T" "is" ($#v2_struct_0 :::"empty"::: ) )) ")" ) otherwise (Bool "(" (Bool "S" "is" ($#v2_struct_0 :::"empty"::: ) ) & (Bool "T" "is" ($#v2_struct_0 :::"empty"::: ) ) ")" ); end; :: deftheorem defines :::"isomorphic"::: WAYBEL_0:def 38 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "S")) "is" ($#v2_struct_0 :::"empty"::: ) )) & (Bool (Bool "not" (Set (Var "T")) "is" ($#v2_struct_0 :::"empty"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "f")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) ) & (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_funct_1 :::"""::: ) )) & (Bool (Set (Var "g")) "is" ($#v5_orders_3 :::"monotone"::: ) ) ")" )) ")" ) ")" ) ")" & "(" (Bool (Bool "(" (Bool (Set (Var "S")) "is" ($#v2_struct_0 :::"empty"::: ) ) "or" (Bool (Set (Var "T")) "is" ($#v2_struct_0 :::"empty"::: ) ) ")" )) "implies" (Bool "(" (Bool (Set (Var "f")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) ) "iff" (Bool "(" (Bool (Set (Var "S")) "is" ($#v2_struct_0 :::"empty"::: ) ) & (Bool (Set (Var "T")) "is" ($#v2_struct_0 :::"empty"::: ) ) ")" ) ")" ) ")" ")" ))); theorem :: WAYBEL_0:66 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T")))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) "iff" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) ")" ) ")" ) ")" ) ")" ))) ; registrationlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")) ($#v23_waybel_0 :::"isomorphic"::: ) -> ($#v2_funct_1 :::"one-to-one"::: ) ($#v5_orders_3 :::"monotone"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T"))))); end; theorem :: WAYBEL_0:67 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_funct_1 :::"""::: ) ) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k2_funct_1 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) ")" ))) ; theorem :: WAYBEL_0:68 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) )) "holds" (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_funct_1 :::"""::: ) ))) "holds" (Bool (Set (Var "g")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) )))) ; theorem :: WAYBEL_0:69 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "f")) ($#r3_waybel_0 :::"preserves_inf_of"::: ) (Set (Var "X"))) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) ))) ; theorem :: WAYBEL_0:70 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Filter":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "f")) ($#r3_waybel_0 :::"preserves_inf_of"::: ) (Set (Var "X"))) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v21_waybel_0 :::"filtered-infs-preserving"::: ) ))) ; theorem :: WAYBEL_0:71 (Bool "for" (Set (Var "S")) "being" ($#l1_orders_2 :::"Semilattice":::) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "f")) ($#r3_waybel_0 :::"preserves_inf_of"::: ) (Set (Var "X"))) ")" ) & (Bool "(" "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_waybel_0 :::"filtered"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "f")) ($#r3_waybel_0 :::"preserves_inf_of"::: ) (Set (Var "X"))) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v17_waybel_0 :::"infs-preserving"::: ) )))) ; theorem :: WAYBEL_0:72 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "f")) ($#r4_waybel_0 :::"preserves_sup_of"::: ) (Set (Var "X"))) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) ))) ; theorem :: WAYBEL_0:73 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Ideal":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "f")) ($#r4_waybel_0 :::"preserves_sup_of"::: ) (Set (Var "X"))) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ))) ; theorem :: WAYBEL_0:74 (Bool "for" (Set (Var "S")) "being" ($#l1_orders_2 :::"sup-Semilattice":::) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool "(" "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "f")) ($#r4_waybel_0 :::"preserves_sup_of"::: ) (Set (Var "X"))) ")" ) & (Bool "(" "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool (Set (Var "f")) ($#r4_waybel_0 :::"preserves_sup_of"::: ) (Set (Var "X"))) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v18_waybel_0 :::"sups-preserving"::: ) )))) ; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; attr "L" is :::"up-complete"::: means :: WAYBEL_0:def 39 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" "L" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool (Set (Var "y")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set (Var "y"))) ")" ) ")" ))); end; :: deftheorem defines :::"up-complete"::: WAYBEL_0:def 39 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v24_waybel_0 :::"up-complete"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "y")) ($#r2_lattice3 :::"is_>=_than"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set (Var "y"))) ")" ) ")" ))) ")" )); registration cluster ($#v3_orders_2 :::"reflexive"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v24_waybel_0 :::"up-complete"::: ) -> ($#v3_orders_2 :::"reflexive"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_yellow_0 :::"upper-bounded"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; theorem :: WAYBEL_0:75 (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"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v24_waybel_0 :::"up-complete"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) ")" )) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; attr "L" is :::"/\-complete"::: means :: WAYBEL_0:def 40 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" "L" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool (Set (Var "y")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) ($#r1_orders_2 :::">="::: ) (Set (Var "y"))) ")" ) ")" ))); end; :: deftheorem defines :::"/\-complete"::: WAYBEL_0:def 40 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v25_waybel_0 :::"/\-complete"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "y")) ($#r1_lattice3 :::"is_<=_than"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) ($#r1_orders_2 :::">="::: ) (Set (Var "y"))) ")" ) ")" ))) ")" )); theorem :: WAYBEL_0:76 (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"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v25_waybel_0 :::"/\-complete"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set (Var "X")) "," (Set (Var "L")))) ")" )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v3_lattice3 :::"complete"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v24_waybel_0 :::"up-complete"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v24_waybel_0 :::"up-complete"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_yellow_0 :::"upper-bounded"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_yellow_0 :::"upper-bounded"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) bbbadV2_ORDERS_2() ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v3_lattice3 :::"complete"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end;