:: WAYBEL_9 semantic presentation begin registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k3_struct_0 :::"id"::: ) "L") -> ($#v5_orders_3 :::"monotone"::: ) ; end; 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")); redefine attr "f" is :::"antitone"::: means :: WAYBEL_9:def 1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "S" "st" (Bool (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y")))) "holds" (Bool (Set "f" ($#k2_yellow_6 :::"."::: ) (Set (Var "x"))) ($#r1_orders_2 :::">="::: ) (Set "f" ($#k2_yellow_6 :::"."::: ) (Set (Var "y"))))); end; :: deftheorem defines :::"antitone"::: WAYBEL_9:def 1 : (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" ($#v5_waybel_0 :::"antitone"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_yellow_6 :::"."::: ) (Set (Var "x"))) ($#r1_orders_2 :::">="::: ) (Set (Set (Var "f")) ($#k2_yellow_6 :::"."::: ) (Set (Var "y"))))) ")" ))); theorem :: WAYBEL_9:1 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "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 "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "L")) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "S"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "K"))) "#)" )) & (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L"))) "#)" )) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool (Set (Var "f")) "is" ($#v5_orders_3 :::"monotone"::: ) )) "holds" (Bool (Set (Var "g")) "is" ($#v5_orders_3 :::"monotone"::: ) ))))) ; theorem :: WAYBEL_9:2 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "K")) "," (Set (Var "L")) "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 "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "K")) "," (Set (Var "L")) "st" (Bool (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "S"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "K"))) "#)" )) & (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L"))) "#)" )) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool (Set (Var "f")) "is" ($#v5_waybel_0 :::"antitone"::: ) )) "holds" (Bool (Set (Var "g")) "is" ($#v5_waybel_0 :::"antitone"::: ) ))))) ; theorem :: WAYBEL_9:3 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "B")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "B")))) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set (Var "F")) "is" ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "A")))) "holds" (Bool (Set (Var "G")) "is" ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "B")))))) ; theorem :: WAYBEL_9:4 (Bool "for" (Set (Var "L")) "being" ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k2_yellow_4 :::""\/""::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "L")) ")" ))))) ; theorem :: WAYBEL_9:5 (Bool "for" (Set (Var "L")) "being" ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k4_yellow_4 :::""/\""::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "L")) ")" ))))) ; theorem :: WAYBEL_9:6 (Bool "for" (Set (Var "L")) "being" ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "y")) ($#k4_waybel_1 :::""/\""::: ) ")" ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: WAYBEL_9:7 (Bool "for" (Set (Var "L")) "being" ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k4_waybel_1 :::""/\""::: ) ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x")))))) ; theorem :: WAYBEL_9:8 (Bool "for" (Set (Var "T")) "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 "T")) "holds" (Bool (Set (Var "N")) ($#r1_waybel_0 :::"is_eventually_in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N"))))))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); let "n" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "D")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "L"))); cluster (Set ($#g1_waybel_0 :::"NetStr"::: ) "(#" "D" "," (Set "(" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "L") ($#k1_toler_1 :::"|_2"::: ) "D" ")" ) "," "n" "#)" ) -> ($#v7_waybel_0 :::"directed"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); let "n" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "D")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "L"))); cluster (Set ($#g1_waybel_0 :::"NetStr"::: ) "(#" "D" "," (Set "(" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "L") ($#k1_toler_1 :::"|_2"::: ) "D" ")" ) "," "n" "#)" ) -> ($#v4_orders_2 :::"transitive"::: ) ; end; theorem :: WAYBEL_9:9 (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"::: ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "N")) "is" ($#v10_waybel_0 :::"eventually-directed"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k11_lattice3 :::""/\""::: ) (Set "(" ($#k1_waybel_2 :::"sup"::: ) (Set (Var "N")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set "(" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k3_yellow_4 :::""/\""::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k1_waybel_0 :::"netmap"::: ) "(" (Set (Var "N")) "," (Set (Var "L")) ")" ")" ) ")" ) ")" )))) ")" )) "holds" (Bool (Set (Var "L")) "is" ($#v1_waybel_2 :::"satisfying_MC"::: ) )) ; theorem :: WAYBEL_9:10 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k3_waybel_2 :::""/\""::: ) (Set (Var "N"))) "is" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L")))))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); let "N" be ($#l1_waybel_0 :::"net":::) "of" (Set (Const "L")); cluster (Set "x" ($#k3_waybel_2 :::""/\""::: ) "N") -> ($#v4_orders_2 :::"transitive"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); let "N" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Const "L")); cluster (Set "x" ($#k3_waybel_2 :::""/\""::: ) "N") -> ($#v3_orders_2 :::"reflexive"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); let "N" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Const "L")); cluster (Set "x" ($#k3_waybel_2 :::""/\""::: ) "N") -> ($#v5_orders_2 :::"antisymmetric"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); let "N" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Const "L")); cluster (Set "x" ($#k3_waybel_2 :::""/\""::: ) "N") -> ($#v4_orders_2 :::"transitive"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "J" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "J")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "L"))); cluster (Set ($#k2_waybel_2 :::"FinSups"::: ) "f") -> ($#v4_orders_2 :::"transitive"::: ) ; end; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "N" be ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Const "L")); func :::"inf"::: "N" -> ($#m1_subset_1 :::"Element":::) "of" "L" equals :: WAYBEL_9:def 2 (Set ($#k5_yellow_2 :::"Inf"::: ) ); end; :: deftheorem defines :::"inf"::: WAYBEL_9:def 2 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L")) "holds" (Bool (Set ($#k1_waybel_9 :::"inf"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set ($#k5_yellow_2 :::"Inf"::: ) )))); definitionlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; let "N" be ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Const "L")); pred :::"ex_sup_of"::: "N" means :: WAYBEL_9:def 3 (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" "N")) "," "L"); pred :::"ex_inf_of"::: "N" means :: WAYBEL_9:def 4 (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" "N")) "," "L"); end; :: deftheorem defines :::"ex_sup_of"::: WAYBEL_9:def 3 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L")) "holds" (Bool "(" (Bool ($#r1_waybel_9 :::"ex_sup_of"::: ) (Set (Var "N"))) "iff" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N")))) "," (Set (Var "L"))) ")" ))); :: deftheorem defines :::"ex_inf_of"::: WAYBEL_9:def 4 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L")) "holds" (Bool "(" (Bool ($#r2_waybel_9 :::"ex_inf_of"::: ) (Set (Var "N"))) "iff" (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N")))) "," (Set (Var "L"))) ")" ))); definitionlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; func "L" :::"+id"::: -> ($#v6_waybel_0 :::"strict"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" "L" means :: WAYBEL_9:def 5 (Bool "(" (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" it) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "L") "#)" )) & (Bool (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k3_struct_0 :::"id"::: ) "L")) ")" ); end; :: deftheorem defines :::"+id"::: WAYBEL_9:def 5 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v6_waybel_0 :::"strict"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k2_waybel_9 :::"+id"::: ) )) "iff" (Bool "(" (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "b2"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L"))) "#)" )) & (Bool (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "L")))) ")" ) ")" ))); registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "L" ($#k2_waybel_9 :::"+id"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_waybel_0 :::"strict"::: ) ; end; registrationlet "L" be ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "L" ($#k2_waybel_9 :::"+id"::: ) ) -> ($#v3_orders_2 :::"reflexive"::: ) ($#v6_waybel_0 :::"strict"::: ) ; end; registrationlet "L" be ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "L" ($#k2_waybel_9 :::"+id"::: ) ) -> ($#v5_orders_2 :::"antisymmetric"::: ) ($#v6_waybel_0 :::"strict"::: ) ; end; registrationlet "L" be ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "L" ($#k2_waybel_9 :::"+id"::: ) ) -> ($#v4_orders_2 :::"transitive"::: ) ($#v6_waybel_0 :::"strict"::: ) ; end; registrationlet "L" be ($#v1_lattice3 :::"with_suprema"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "L" ($#k2_waybel_9 :::"+id"::: ) ) -> ($#v6_waybel_0 :::"strict"::: ) ($#v7_waybel_0 :::"directed"::: ) ; end; registrationlet "L" be ($#v7_waybel_0 :::"directed"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "L" ($#k2_waybel_9 :::"+id"::: ) ) -> ($#v6_waybel_0 :::"strict"::: ) ($#v7_waybel_0 :::"directed"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "L" ($#k2_waybel_9 :::"+id"::: ) ) -> ($#v6_waybel_0 :::"strict"::: ) ($#v8_waybel_0 :::"monotone"::: ) ($#v10_waybel_0 :::"eventually-directed"::: ) ; end; definitionlet "L" be ($#l1_orders_2 :::"RelStr"::: ) ; func "L" :::"opp+id"::: -> ($#v6_waybel_0 :::"strict"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" "L" means :: WAYBEL_9:def 6 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "L") ($#k3_relset_1 :::"~"::: ) )) & (Bool (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k3_struct_0 :::"id"::: ) "L")) ")" ); end; :: deftheorem defines :::"opp+id"::: WAYBEL_9:def 6 : (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v6_waybel_0 :::"strict"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k3_waybel_9 :::"opp+id"::: ) )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L")))) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L"))) ($#k3_relset_1 :::"~"::: ) )) & (Bool (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "L")))) ")" ) ")" ))); theorem :: WAYBEL_9:11 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "L")) ($#k7_lattice3 :::"~"::: ) ")" )) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" (Set (Var "L")) ($#k7_lattice3 :::"~"::: ) ")" )) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "L")) ($#k3_waybel_9 :::"opp+id"::: ) ")" )) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" (Set (Var "L")) ($#k3_waybel_9 :::"opp+id"::: ) ")" )) "#)" ))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "L" ($#k3_waybel_9 :::"opp+id"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_waybel_0 :::"strict"::: ) ; end; registrationlet "L" be ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "L" ($#k3_waybel_9 :::"opp+id"::: ) ) -> ($#v3_orders_2 :::"reflexive"::: ) ($#v6_waybel_0 :::"strict"::: ) ; end; registrationlet "L" be ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "L" ($#k3_waybel_9 :::"opp+id"::: ) ) -> ($#v5_orders_2 :::"antisymmetric"::: ) ($#v6_waybel_0 :::"strict"::: ) ; end; registrationlet "L" be ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "L" ($#k3_waybel_9 :::"opp+id"::: ) ) -> ($#v4_orders_2 :::"transitive"::: ) ($#v6_waybel_0 :::"strict"::: ) ; end; registrationlet "L" be ($#v2_lattice3 :::"with_infima"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "L" ($#k3_waybel_9 :::"opp+id"::: ) ) -> ($#v6_waybel_0 :::"strict"::: ) ($#v7_waybel_0 :::"directed"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "L" ($#k3_waybel_9 :::"opp+id"::: ) ) -> ($#v6_waybel_0 :::"strict"::: ) ($#v9_waybel_0 :::"antitone"::: ) ($#v11_waybel_0 :::"eventually-filtered"::: ) ; 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")); let "i" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "N")); func "N" :::"|"::: "i" -> ($#v6_waybel_0 :::"strict"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" "L" means :: WAYBEL_9:def 7 (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it)) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "N" "st" (Bool "(" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool "i" ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) ")" )) ")" ) ")" ) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" it) ($#r2_relset_1 :::"="::: ) (Set (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "N") ($#k1_toler_1 :::"|_2"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it))) & (Bool (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" "N") ($#k2_partfun1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it))) ")" ); end; :: deftheorem defines :::"|"::: WAYBEL_9: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")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) (Bool "for" (Set (Var "b4")) "being" ($#v6_waybel_0 :::"strict"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k4_waybel_9 :::"|"::: ) (Set (Var "i")))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4")))) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "st" (Bool "(" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "i")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) ")" )) ")" ) ")" ) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "b4"))) ($#r2_relset_1 :::"="::: ) (Set (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "N"))) ($#k1_toler_1 :::"|_2"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4"))))) & (Bool (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N"))) ($#k2_partfun1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4"))))) ")" ) ")" ))))); theorem :: WAYBEL_9: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 "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "N")) ($#k4_waybel_9 :::"|"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) : (Bool (Set (Var "i")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) "}" )))) ; theorem :: WAYBEL_9:13 (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 "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "N")) ($#k4_waybel_9 :::"|"::: ) (Set (Var "i")) ")" )) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))))))) ; theorem :: WAYBEL_9:14 (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")) ($#k4_waybel_9 :::"|"::: ) (Set (Var "i"))) "is" ($#v2_yellow_6 :::"full"::: ) ($#m1_yellow_6 :::"SubNetStr"::: ) "of" (Set (Var "N")))))) ; registrationlet "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"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Const "L")); let "i" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "N")); cluster (Set "N" ($#k4_waybel_9 :::"|"::: ) "i") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v6_waybel_0 :::"strict"::: ) ; end; registrationlet "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"::: ) ) ($#v7_waybel_0 :::"directed"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Const "L")); let "i" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "N")); cluster (Set "N" ($#k4_waybel_9 :::"|"::: ) "i") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_waybel_0 :::"strict"::: ) ; end; registrationlet "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"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Const "L")); let "i" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "N")); cluster (Set "N" ($#k4_waybel_9 :::"|"::: ) "i") -> ($#v5_orders_2 :::"antisymmetric"::: ) ($#v6_waybel_0 :::"strict"::: ) ; end; registrationlet "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"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v7_waybel_0 :::"directed"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Const "L")); let "i" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "N")); cluster (Set "N" ($#k4_waybel_9 :::"|"::: ) "i") -> ($#v5_orders_2 :::"antisymmetric"::: ) ($#v6_waybel_0 :::"strict"::: ) ; end; registrationlet "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"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Const "L")); let "i" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "N")); cluster (Set "N" ($#k4_waybel_9 :::"|"::: ) "i") -> ($#v4_orders_2 :::"transitive"::: ) ($#v6_waybel_0 :::"strict"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "N" be ($#l1_waybel_0 :::"net":::) "of" (Set (Const "L")); let "i" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "N")); cluster (Set "N" ($#k4_waybel_9 :::"|"::: ) "i") -> ($#v4_orders_2 :::"transitive"::: ) ($#v6_waybel_0 :::"strict"::: ) ($#v7_waybel_0 :::"directed"::: ) ; end; theorem :: WAYBEL_9:15 (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"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L")) (Bool "for" (Set (Var "i")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "N")) ($#k4_waybel_9 :::"|"::: ) (Set (Var "i")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) "holds" (Bool (Set (Set (Var "N")) ($#k2_waybel_0 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "N")) ($#k4_waybel_9 :::"|"::: ) (Set (Var "i")) ")" ) ($#k2_waybel_0 :::"."::: ) (Set (Var "x1")))))))) ; theorem :: WAYBEL_9:16 (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"::: ) ) ($#v7_waybel_0 :::"directed"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L")) (Bool "for" (Set (Var "i")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "N")) ($#k4_waybel_9 :::"|"::: ) (Set (Var "i")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) "holds" (Bool (Set (Set (Var "N")) ($#k2_waybel_0 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "N")) ($#k4_waybel_9 :::"|"::: ) (Set (Var "i")) ")" ) ($#k2_waybel_0 :::"."::: ) (Set (Var "x1")))))))) ; theorem :: WAYBEL_9:17 (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" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "holds" (Bool (Set (Set (Var "N")) ($#k4_waybel_9 :::"|"::: ) (Set (Var "i"))) "is" ($#m2_yellow_6 :::"subnet"::: ) "of" (Set (Var "N")))))) ; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "N" be ($#l1_waybel_0 :::"net":::) "of" (Set (Const "T")); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#v6_waybel_0 :::"strict"::: ) ($#v7_waybel_0 :::"directed"::: ) for ($#m2_yellow_6 :::"subnet"::: ) "of" "N"; end; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "N" be ($#l1_waybel_0 :::"net":::) "of" (Set (Const "L")); let "i" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "N")); :: original: :::"|"::: redefine func "N" :::"|"::: "i" -> ($#v6_waybel_0 :::"strict"::: ) ($#m2_yellow_6 :::"subnet"::: ) "of" "N"; end; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "T" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); let "N" be ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Const "S")); func "f" :::"*"::: "N" -> ($#v6_waybel_0 :::"strict"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" "T" means :: WAYBEL_9:def 8 (Bool "(" (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" it) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "N") "#)" )) & (Bool (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_partfun1 :::"*"::: ) (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" "N"))) ")" ); end; :: deftheorem defines :::"*"::: WAYBEL_9:def 8 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "T")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "b5")) "being" ($#v6_waybel_0 :::"strict"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k6_waybel_9 :::"*"::: ) (Set (Var "N")))) "iff" (Bool "(" (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b5"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "b5"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "N"))) "#)" )) & (Bool (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N"))))) ")" ) ")" )))))); registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "T" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); let "N" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Const "S")); cluster (Set "f" ($#k6_waybel_9 :::"*"::: ) "N") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_waybel_0 :::"strict"::: ) ; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "T" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); let "N" be ($#v3_orders_2 :::"reflexive"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Const "S")); cluster (Set "f" ($#k6_waybel_9 :::"*"::: ) "N") -> ($#v3_orders_2 :::"reflexive"::: ) ($#v6_waybel_0 :::"strict"::: ) ; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "T" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); let "N" be ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Const "S")); cluster (Set "f" ($#k6_waybel_9 :::"*"::: ) "N") -> ($#v5_orders_2 :::"antisymmetric"::: ) ($#v6_waybel_0 :::"strict"::: ) ; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "T" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); let "N" be ($#v4_orders_2 :::"transitive"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Const "S")); cluster (Set "f" ($#k6_waybel_9 :::"*"::: ) "N") -> ($#v4_orders_2 :::"transitive"::: ) ($#v6_waybel_0 :::"strict"::: ) ; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "T" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); let "N" be ($#v7_waybel_0 :::"directed"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Const "S")); cluster (Set "f" ($#k6_waybel_9 :::"*"::: ) "N") -> ($#v6_waybel_0 :::"strict"::: ) ($#v7_waybel_0 :::"directed"::: ) ; end; theorem :: WAYBEL_9:18 (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")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k4_waybel_1 :::""/\""::: ) ")" ) ($#k6_waybel_9 :::"*"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_waybel_2 :::""/\""::: ) (Set (Var "N"))))))) ; begin theorem :: WAYBEL_9:19 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "S"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) "#)" )) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set (Var "F")) "is" ($#v1_tops_2 :::"open"::: ) )) "holds" (Bool (Set (Var "G")) "is" ($#v1_tops_2 :::"open"::: ) )))) ; theorem :: WAYBEL_9:20 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "S"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) "#)" )) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set (Var "F")) "is" ($#v2_tops_2 :::"closed"::: ) )) "holds" (Bool (Set (Var "G")) "is" ($#v2_tops_2 :::"closed"::: ) )))) ; definitionattr "c1" is :::"strict"::: ; struct :::"TopRelStr"::: -> ($#l1_pre_topc :::"TopStruct"::: ) "," ($#l1_orders_2 :::"RelStr"::: ) ; aggr :::"TopRelStr":::(# :::"carrier":::, :::"InternalRel":::, :::"topology"::: #) -> ($#l1_waybel_9 :::"TopRelStr"::: ) ; end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "A")) "," (Set (Const "A")); let "T" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "A")); cluster (Set ($#g1_waybel_9 :::"TopRelStr"::: ) "(#" "A" "," "R" "," "T" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; registrationlet "x" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k1_tarski :::"{"::: ) (Set (Const "x")) ($#k1_tarski :::"}"::: ) ); let "T" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set ($#k1_tarski :::"{"::: ) (Set (Const "x")) ($#k1_tarski :::"}"::: ) ); cluster (Set ($#g1_waybel_9 :::"TopRelStr"::: ) "(#" (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) "," "R" "," "T" "#)" ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "O" be ($#m1_subset_1 :::"Order":::) "of" (Set (Const "X")); let "T" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); cluster (Set ($#g1_waybel_9 :::"TopRelStr"::: ) "(#" "X" "," "O" "," "T" "#)" ) -> ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ; end; registration cluster ($#v8_struct_0 :::"finite"::: ) (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v1_tdlat_3 :::"discrete"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v1_waybel_9 :::"strict"::: ) for ($#l1_waybel_9 :::"TopRelStr"::: ) ; end; definitionmode TopLattice is ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#l1_waybel_9 :::"TopRelStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v8_pre_topc :::"Hausdorff"::: ) ($#v1_tdlat_3 :::"discrete"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v1_compts_1 :::"compact"::: ) ($#v1_waybel_9 :::"strict"::: ) for ($#l1_waybel_9 :::"TopRelStr"::: ) ; end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_pre_topc :::"Hausdorff"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_pre_topc :::"Hausdorff"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "T"; end; theorem :: WAYBEL_9:21 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_yellow_6 :::"OpenNeighborhoods"::: ) (Set (Var "p")) ")" ) "holds" (Bool (Set (Var "A")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "p")))))) ; theorem :: WAYBEL_9:22 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_yellow_6 :::"OpenNeighborhoods"::: ) (Set (Var "p")) ")" ) "holds" (Bool (Set (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "B"))) "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_yellow_6 :::"OpenNeighborhoods"::: ) (Set (Var "p")) ")" ))))) ; theorem :: WAYBEL_9:23 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_yellow_6 :::"OpenNeighborhoods"::: ) (Set (Var "p")) ")" ) "holds" (Bool (Set (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B"))) "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_yellow_6 :::"OpenNeighborhoods"::: ) (Set (Var "p")) ")" ))))) ; theorem :: WAYBEL_9:24 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k10_yellow_6 :::"Lim"::: ) (Set (Var "N"))))) "holds" (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N")))))) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "S")))))))) ; theorem :: WAYBEL_9:25 (Bool "for" (Set (Var "T")) "being" ($#v8_pre_topc :::"Hausdorff"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "N")) "being" ($#v3_yellow_6 :::"convergent"::: ) ($#l1_waybel_0 :::"net":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k2_yellow_6 :::"."::: ) (Set "(" ($#k11_yellow_6 :::"lim"::: ) (Set (Var "N")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k10_yellow_6 :::"Lim"::: ) (Set "(" (Set (Var "f")) ($#k6_waybel_9 :::"*"::: ) (Set (Var "N")) ")" )))))) ; theorem :: WAYBEL_9:26 (Bool "for" (Set (Var "T")) "being" ($#v8_pre_topc :::"Hausdorff"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "N")) "being" ($#v3_yellow_6 :::"convergent"::: ) ($#l1_waybel_0 :::"net":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Set (Var "x")) ($#k4_waybel_1 :::""/\""::: ) ) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k12_lattice3 :::""/\""::: ) (Set "(" ($#k11_yellow_6 :::"lim"::: ) (Set (Var "N")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k10_yellow_6 :::"Lim"::: ) (Set "(" (Set (Var "x")) ($#k3_waybel_2 :::""/\""::: ) (Set (Var "N")) ")" )))))) ; theorem :: WAYBEL_9:27 (Bool "for" (Set (Var "S")) "being" ($#v8_pre_topc :::"Hausdorff"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "a")) ($#k4_waybel_1 :::""/\""::: ) ) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" )) "holds" (Bool (Set ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x"))) "is" ($#v4_pre_topc :::"closed"::: ) ))) ; theorem :: WAYBEL_9:28 (Bool "for" (Set (Var "S")) "being" ($#v8_pre_topc :::"Hausdorff"::: ) ($#v1_compts_1 :::"compact"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "b")) ($#k4_waybel_1 :::""/\""::: ) ) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" )) "holds" (Bool (Set ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x"))) "is" ($#v4_pre_topc :::"closed"::: ) ))) ; begin definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "N" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Const "T")); let "p" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); pred "p" :::"is_a_cluster_point_of"::: "N" means :: WAYBEL_9:def 9 (Bool "for" (Set (Var "O")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" "p" "holds" (Bool "N" ($#r2_waybel_0 :::"is_often_in"::: ) (Set (Var "O")))); end; :: deftheorem defines :::"is_a_cluster_point_of"::: WAYBEL_9:def 9 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "T")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r3_waybel_9 :::"is_a_cluster_point_of"::: ) (Set (Var "N"))) "iff" (Bool "for" (Set (Var "O")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "p")) "holds" (Bool (Set (Var "N")) ($#r2_waybel_0 :::"is_often_in"::: ) (Set (Var "O")))) ")" )))); theorem :: WAYBEL_9:29 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k10_yellow_6 :::"Lim"::: ) (Set (Var "N"))))) "holds" (Bool (Set (Var "c")) ($#r3_waybel_9 :::"is_a_cluster_point_of"::: ) (Set (Var "N")))))) ; theorem :: WAYBEL_9:30 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_pre_topc :::"Hausdorff"::: ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "T")) (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Set (Var "c")) ($#r3_waybel_9 :::"is_a_cluster_point_of"::: ) (Set (Var "N")))))) ; theorem :: WAYBEL_9:31 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "M")) "being" ($#m2_yellow_6 :::"subnet"::: ) "of" (Set (Var "N")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "c")) ($#r3_waybel_9 :::"is_a_cluster_point_of"::: ) (Set (Var "M")))) "holds" (Bool (Set (Var "c")) ($#r3_waybel_9 :::"is_a_cluster_point_of"::: ) (Set (Var "N"))))))) ; theorem :: WAYBEL_9:32 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "x")) ($#r3_waybel_9 :::"is_a_cluster_point_of"::: ) (Set (Var "N")))) "holds" (Bool "ex" (Set (Var "M")) "being" ($#m2_yellow_6 :::"subnet"::: ) "of" (Set (Var "N")) "st" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_yellow_6 :::"Lim"::: ) (Set (Var "M")))))))) ; theorem :: WAYBEL_9:33 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_pre_topc :::"Hausdorff"::: ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "c")) ($#r3_waybel_9 :::"is_a_cluster_point_of"::: ) (Set (Var "N"))) & (Bool (Set (Var "d")) ($#r3_waybel_9 :::"is_a_cluster_point_of"::: ) (Set (Var "N")))) "holds" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "d"))) ")" )) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "s")) ($#r3_waybel_9 :::"is_a_cluster_point_of"::: ) (Set (Var "N")))) "holds" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k10_yellow_6 :::"Lim"::: ) (Set (Var "N"))))))) ; theorem :: WAYBEL_9:34 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "c")) ($#r3_waybel_9 :::"is_a_cluster_point_of"::: ) (Set (Var "N"))) & (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N")))) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))))) ; theorem :: WAYBEL_9:35 (Bool "for" (Set (Var "S")) "being" ($#v8_pre_topc :::"Hausdorff"::: ) ($#v1_compts_1 :::"compact"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "S")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "x")) ($#k4_waybel_1 :::""/\""::: ) ) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" ) & (Bool (Set (Var "N")) "is" ($#v10_waybel_0 :::"eventually-directed"::: ) ) & (Bool (Set (Var "c")) ($#r3_waybel_9 :::"is_a_cluster_point_of"::: ) (Set (Var "N")))) "holds" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel_2 :::"sup"::: ) (Set (Var "N"))))))) ; theorem :: WAYBEL_9:36 (Bool "for" (Set (Var "S")) "being" ($#v8_pre_topc :::"Hausdorff"::: ) ($#v1_compts_1 :::"compact"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "S")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "x")) ($#k4_waybel_1 :::""/\""::: ) ) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" ) & (Bool (Set (Var "N")) "is" ($#v11_waybel_0 :::"eventually-filtered"::: ) ) & (Bool (Set (Var "c")) ($#r3_waybel_9 :::"is_a_cluster_point_of"::: ) (Set (Var "N")))) "holds" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel_9 :::"inf"::: ) (Set (Var "N"))))))) ; begin theorem :: WAYBEL_9:37 (Bool "for" (Set (Var "S")) "being" ($#v8_pre_topc :::"Hausdorff"::: ) ($#l1_waybel_9 :::"TopLattice":::) "st" (Bool (Bool "(" "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "N")) "is" ($#v10_waybel_0 :::"eventually-directed"::: ) )) "holds" (Bool "(" (Bool ($#r1_waybel_9 :::"ex_sup_of"::: ) (Set (Var "N"))) & (Bool (Set ($#k1_waybel_2 :::"sup"::: ) (Set (Var "N"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_yellow_6 :::"Lim"::: ) (Set (Var "N")))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "x")) ($#k4_waybel_1 :::""/\""::: ) ) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" )) "holds" (Bool (Set (Var "S")) "is" ($#v2_waybel_2 :::"meet-continuous"::: ) )) ; theorem :: WAYBEL_9:38 (Bool "for" (Set (Var "S")) "being" ($#v8_pre_topc :::"Hausdorff"::: ) ($#v1_compts_1 :::"compact"::: ) ($#l1_waybel_9 :::"TopLattice":::) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "x")) ($#k4_waybel_1 :::""/\""::: ) ) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "N")) "is" ($#v10_waybel_0 :::"eventually-directed"::: ) )) "holds" (Bool "(" (Bool ($#r1_waybel_9 :::"ex_sup_of"::: ) (Set (Var "N"))) & (Bool (Set ($#k1_waybel_2 :::"sup"::: ) (Set (Var "N"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_yellow_6 :::"Lim"::: ) (Set (Var "N")))) ")" ))) ; theorem :: WAYBEL_9:39 (Bool "for" (Set (Var "S")) "being" ($#v8_pre_topc :::"Hausdorff"::: ) ($#v1_compts_1 :::"compact"::: ) ($#l1_waybel_9 :::"TopLattice":::) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "x")) ($#k4_waybel_1 :::""/\""::: ) ) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "N")) "is" ($#v11_waybel_0 :::"eventually-filtered"::: ) )) "holds" (Bool "(" (Bool ($#r2_waybel_9 :::"ex_inf_of"::: ) (Set (Var "N"))) & (Bool (Set ($#k1_waybel_9 :::"inf"::: ) (Set (Var "N"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_yellow_6 :::"Lim"::: ) (Set (Var "N")))) ")" ))) ; theorem :: WAYBEL_9:40 (Bool "for" (Set (Var "S")) "being" ($#v8_pre_topc :::"Hausdorff"::: ) ($#v1_compts_1 :::"compact"::: ) ($#l1_waybel_9 :::"TopLattice":::) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "x")) ($#k4_waybel_1 :::""/\""::: ) ) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" )) "holds" (Bool (Set (Var "S")) "is" ($#v3_yellow_0 :::"bounded"::: ) )) ; theorem :: WAYBEL_9:41 (Bool "for" (Set (Var "S")) "being" ($#v8_pre_topc :::"Hausdorff"::: ) ($#v1_compts_1 :::"compact"::: ) ($#l1_waybel_9 :::"TopLattice":::) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "x")) ($#k4_waybel_1 :::""/\""::: ) ) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" )) "holds" (Bool (Set (Var "S")) "is" ($#v2_waybel_2 :::"meet-continuous"::: ) )) ;