:: WAYBEL28 semantic presentation begin theorem :: WAYBEL28:1 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k1_waybel_9 :::"inf"::: ) (Set (Var "N"))) ($#r3_orders_2 :::"<="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N")))))) ; theorem :: WAYBEL28:2 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool "(" "for" (Set (Var "M")) "being" ($#m2_yellow_6 :::"subnet"::: ) "of" (Set (Var "N")) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "M")))) ")" )) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N")))) & (Bool "(" "for" (Set (Var "M")) "being" ($#m2_yellow_6 :::"subnet"::: ) "of" (Set (Var "N")) "holds" (Bool (Set (Var "x")) ($#r1_orders_2 :::">="::: ) (Set ($#k1_waybel_9 :::"inf"::: ) (Set (Var "M")))) ")" ) ")" )))) ; theorem :: WAYBEL28:3 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "N")) ($#r2_hidden :::"in"::: ) (Set ($#k6_yellow_6 :::"NetUniv"::: ) (Set (Var "L")))) & (Bool "(" "for" (Set (Var "M")) "being" ($#m2_yellow_6 :::"subnet"::: ) "of" (Set (Var "N")) "st" (Bool (Bool (Set (Var "M")) ($#r2_hidden :::"in"::: ) (Set ($#k6_yellow_6 :::"NetUniv"::: ) (Set (Var "L"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "M")))) ")" )) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N")))) & (Bool "(" "for" (Set (Var "M")) "being" ($#m2_yellow_6 :::"subnet"::: ) "of" (Set (Var "N")) "st" (Bool (Bool (Set (Var "M")) ($#r2_hidden :::"in"::: ) (Set ($#k6_yellow_6 :::"NetUniv"::: ) (Set (Var "L"))))) "holds" (Bool (Set (Var "x")) ($#r1_orders_2 :::">="::: ) (Set ($#k1_waybel_9 :::"inf"::: ) (Set (Var "M")))) ")" ) ")" )))) ; definitionlet "N" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "N")) "," (Set (Const "N")); attr "f" is :::"greater_or_equal_to_id"::: means :: WAYBEL28:def 1 (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" "N" "holds" (Bool (Set (Var "j")) ($#r1_orders_2 :::"<="::: ) (Set "f" ($#k2_yellow_6 :::"."::: ) (Set (Var "j"))))); end; :: deftheorem defines :::"greater_or_equal_to_id"::: WAYBEL28:def 1 : (Bool "for" (Set (Var "N")) "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 "N")) "," (Set (Var "N")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_waybel28 :::"greater_or_equal_to_id"::: ) ) "iff" (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "holds" (Bool (Set (Var "j")) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "f")) ($#k2_yellow_6 :::"."::: ) (Set (Var "j"))))) ")" ))); theorem :: WAYBEL28:4 (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "N"))) "is" ($#v1_waybel28 :::"greater_or_equal_to_id"::: ) )) ; theorem :: WAYBEL28:5 (Bool "for" (Set (Var "N")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_waybel_0 :::"directed"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "z"))) & (Bool (Set (Var "y")) ($#r1_orders_2 :::"<="::: ) (Set (Var "z"))) ")" )))) ; registrationlet "N" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_waybel_0 :::"directed"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N")) bbbadV1_FUNCT_2((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N")) ($#v1_waybel28 :::"greater_or_equal_to_id"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "N" 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_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N")) bbbadV1_FUNCT_2((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N")) ($#v1_waybel28 :::"greater_or_equal_to_id"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") ($#k2_zfmisc_1 :::":]"::: ) )); 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 "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "N")) "," (Set (Const "N")); func "N" :::"*"::: "f" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_waybel_0 :::"strict"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" "L" means :: WAYBEL28:def 2 (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_funct_2 :::"="::: ) (Set (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" "N") ($#k1_partfun1 :::"*"::: ) "f")) ")" ); end; :: deftheorem defines :::"*"::: WAYBEL28:def 2 : (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 "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "N")) "," (Set (Var "N")) (Bool "for" (Set (Var "b4")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_waybel_0 :::"strict"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k1_waybel28 :::"*"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "b4"))) "#)" ) ($#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 "b4"))) ($#r1_funct_2 :::"="::: ) (Set (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N"))) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")))) ")" ) ")" ))))); theorem :: WAYBEL28:6 (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 "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "N")) "," (Set (Var "N")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "N")) ($#k1_waybel28 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))))))) ; theorem :: WAYBEL28: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 "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "N")) "," (Set (Var "N")) "holds" (Bool (Set (Set (Var "N")) ($#k1_waybel28 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#g1_waybel_0 :::"NetStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "N"))) "," (Set "(" (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N"))) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) "#)" ))))) ; theorem :: WAYBEL28: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"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#v7_waybel_0 :::"directed"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "holds" (Bool (Set ($#g1_waybel_0 :::"NetStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "N"))) "," (Set (Var "f")) "#)" ) "is" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L")))))) ; 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"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#v7_waybel_0 :::"directed"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "N"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "L"))); cluster (Set ($#g1_waybel_0 :::"NetStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "N") "," "f" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#v7_waybel_0 :::"directed"::: ) ; end; theorem :: WAYBEL28: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" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "N")) "," (Set (Var "N")) "holds" (Bool (Set (Set (Var "N")) ($#k1_waybel28 :::"*"::: ) (Set (Var "p"))) "is" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L")))))) ; 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 "p" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "N")) "," (Set (Const "N")); cluster (Set "N" ($#k1_waybel28 :::"*"::: ) "p") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#v6_waybel_0 :::"strict"::: ) ($#v7_waybel_0 :::"directed"::: ) ; end; theorem :: WAYBEL28: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" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "N")) "," (Set (Var "N")) "st" (Bool (Bool (Set (Var "N")) ($#r2_hidden :::"in"::: ) (Set ($#k6_yellow_6 :::"NetUniv"::: ) (Set (Var "L"))))) "holds" (Bool (Set (Set (Var "N")) ($#k1_waybel28 :::"*"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_yellow_6 :::"NetUniv"::: ) (Set (Var "L"))))))) ; theorem :: WAYBEL28: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")) "," (Set (Var "M")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#g1_waybel_0 :::"NetStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "N"))) "," (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "N"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_waybel_0 :::"NetStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_waybel_0 :::"mapping"::: ) "of" (Set (Var "M"))) "#)" ))) "holds" (Bool (Set (Var "M")) "is" ($#m2_yellow_6 :::"subnet"::: ) "of" (Set (Var "N"))))) ; theorem :: WAYBEL28: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" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "being" ($#v1_waybel28 :::"greater_or_equal_to_id"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "N")) "," (Set (Var "N")) "holds" (Bool (Set (Set (Var "N")) ($#k1_waybel28 :::"*"::: ) (Set (Var "p"))) "is" ($#m2_yellow_6 :::"subnet"::: ) "of" (Set (Var "N")))))) ; 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 "p" be ($#v1_waybel28 :::"greater_or_equal_to_id"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "N")) "," (Set (Const "N")); :: original: :::"*"::: redefine func "N" :::"*"::: "p" -> ($#v6_waybel_0 :::"strict"::: ) ($#m2_yellow_6 :::"subnet"::: ) "of" "N"; end; theorem :: WAYBEL28:13 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "N")) ($#r2_hidden :::"in"::: ) (Set ($#k6_yellow_6 :::"NetUniv"::: ) (Set (Var "L")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N")))) & (Bool "(" "for" (Set (Var "M")) "being" ($#m2_yellow_6 :::"subnet"::: ) "of" (Set (Var "N")) "st" (Bool (Bool (Set (Var "M")) ($#r2_hidden :::"in"::: ) (Set ($#k6_yellow_6 :::"NetUniv"::: ) (Set (Var "L"))))) "holds" (Bool (Set (Var "x")) ($#r1_orders_2 :::">="::: ) (Set ($#k1_waybel_9 :::"inf"::: ) (Set (Var "M")))) ")" )) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N")))) & (Bool "(" "for" (Set (Var "p")) "being" ($#v1_waybel28 :::"greater_or_equal_to_id"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "N")) "," (Set (Var "N")) "holds" (Bool (Set (Var "x")) ($#r1_orders_2 :::">="::: ) (Set ($#k1_waybel_9 :::"inf"::: ) (Set "(" (Set (Var "N")) ($#k2_waybel28 :::"*"::: ) (Set (Var "p")) ")" ))) ")" ) ")" )))) ; theorem :: WAYBEL28:14 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "N")))) & (Bool "(" "for" (Set (Var "p")) "being" ($#v1_waybel28 :::"greater_or_equal_to_id"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "N")) "," (Set (Var "N")) "holds" (Bool (Set (Var "x")) ($#r1_orders_2 :::">="::: ) (Set ($#k1_waybel_9 :::"inf"::: ) (Set "(" (Set (Var "N")) ($#k2_waybel28 :::"*"::: ) (Set (Var "p")) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "M")) "being" ($#m2_yellow_6 :::"subnet"::: ) "of" (Set (Var "N")) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "M")))))))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; func :::"lim_inf-Convergence"::: "L" -> ($#m4_yellow_6 :::"Convergence-Class"::: ) "of" "L" means :: WAYBEL28:def 3 (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" "L" "st" (Bool (Bool (Set (Var "N")) ($#r2_hidden :::"in"::: ) (Set ($#k6_yellow_6 :::"NetUniv"::: ) "L"))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "N")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "for" (Set (Var "M")) "being" ($#m2_yellow_6 :::"subnet"::: ) "of" (Set (Var "N")) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "M"))))) ")" ))); end; :: deftheorem defines :::"lim_inf-Convergence"::: WAYBEL28:def 3 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m4_yellow_6 :::"Convergence-Class"::: ) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_waybel28 :::"lim_inf-Convergence"::: ) (Set (Var "L")))) "iff" (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "N")) ($#r2_hidden :::"in"::: ) (Set ($#k6_yellow_6 :::"NetUniv"::: ) (Set (Var "L"))))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "N")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "for" (Set (Var "M")) "being" ($#m2_yellow_6 :::"subnet"::: ) "of" (Set (Var "N")) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "M"))))) ")" ))) ")" ))); theorem :: WAYBEL28:15 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "N")) ($#r2_hidden :::"in"::: ) (Set ($#k6_yellow_6 :::"NetUniv"::: ) (Set (Var "L"))))) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "N")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_waybel28 :::"lim_inf-Convergence"::: ) (Set (Var "L")))) "iff" (Bool "for" (Set (Var "M")) "being" ($#m2_yellow_6 :::"subnet"::: ) "of" (Set (Var "N")) "st" (Bool (Bool (Set (Var "M")) ($#r2_hidden :::"in"::: ) (Set ($#k6_yellow_6 :::"NetUniv"::: ) (Set (Var "L"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "M"))))) ")" )))) ; theorem :: WAYBEL28:16 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "N")) "being" ($#v1_yellow_6 :::"constant"::: ) ($#l1_waybel_0 :::"net":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "M")) "being" ($#m2_yellow_6 :::"subnet"::: ) "of" (Set (Var "N")) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v1_yellow_6 :::"constant"::: ) ) & (Bool (Set ($#k4_yellow_6 :::"the_value_of"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set ($#k4_yellow_6 :::"the_value_of"::: ) (Set (Var "M")))) ")" )))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; func :::"xi"::: "L" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "L" equals :: WAYBEL28:def 4 (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set "(" ($#k13_yellow_6 :::"ConvergenceSpace"::: ) (Set "(" ($#k3_waybel28 :::"lim_inf-Convergence"::: ) "L" ")" ) ")" )); end; :: deftheorem defines :::"xi"::: WAYBEL28:def 4 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k4_waybel28 :::"xi"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set "(" ($#k13_yellow_6 :::"ConvergenceSpace"::: ) (Set "(" ($#k3_waybel28 :::"lim_inf-Convergence"::: ) (Set (Var "L")) ")" ) ")" )))); theorem :: WAYBEL28:17 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool (Set ($#k3_waybel28 :::"lim_inf-Convergence"::: ) (Set (Var "L"))) "is" ($#v4_yellow_6 :::"(CONSTANTS)"::: ) )) ; theorem :: WAYBEL28:18 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k3_waybel28 :::"lim_inf-Convergence"::: ) (Set (Var "L"))) "is" ($#v5_yellow_6 :::"(SUBNETS)"::: ) )) ; theorem :: WAYBEL28:19 (Bool "for" (Set (Var "L")) "being" ($#v3_waybel_3 :::"continuous"::: ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool (Set ($#k3_waybel28 :::"lim_inf-Convergence"::: ) (Set (Var "L"))) "is" ($#v6_yellow_6 :::"(DIVERGENCE)"::: ) )) ; theorem :: WAYBEL28:20 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "N")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "N")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_waybel28 :::"lim_inf-Convergence"::: ) (Set (Var "L"))))) "holds" (Bool (Set (Var "N")) ($#r2_hidden :::"in"::: ) (Set ($#k6_yellow_6 :::"NetUniv"::: ) (Set (Var "L")))))) ; theorem :: WAYBEL28:21 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m4_yellow_6 :::"Convergence-Class"::: ) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "C1")) ($#r1_tarski :::"c="::: ) (Set (Var "C2")))) "holds" (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set "(" ($#k13_yellow_6 :::"ConvergenceSpace"::: ) (Set (Var "C2")) ")" )) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set "(" ($#k13_yellow_6 :::"ConvergenceSpace"::: ) (Set (Var "C1")) ")" ))))) ; theorem :: WAYBEL28:22 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k3_waybel28 :::"lim_inf-Convergence"::: ) (Set (Var "L"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_waybel11 :::"Scott-Convergence"::: ) (Set (Var "L"))))) ; theorem :: WAYBEL28:23 (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 (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k1_yellow_6 :::"the_universe_of"::: ) (Set (Var "Y"))))) ; theorem :: WAYBEL28: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"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k4_waybel17 :::"Net-Str"::: ) (Set (Var "D"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_yellow_6 :::"NetUniv"::: ) (Set (Var "L")))))) ; theorem :: WAYBEL28:25 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "M")) "being" ($#m2_yellow_6 :::"subnet"::: ) "of" (Set ($#k4_waybel17 :::"Net-Str"::: ) (Set (Var "D"))) "holds" (Bool (Set ($#k1_waybel11 :::"lim_inf"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k1_yellow_0 :::"sup"::: ) (Set (Var "D"))))))) ; theorem :: WAYBEL28:26 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k4_waybel17 :::"Net-Str"::: ) (Set (Var "D")) ")" ) "," (Set "(" ($#k1_yellow_0 :::"sup"::: ) (Set (Var "D")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_waybel28 :::"lim_inf-Convergence"::: ) (Set (Var "L")))))) ; theorem :: WAYBEL28:27 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "U1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "U1")) ($#r2_hidden :::"in"::: ) (Set ($#k4_waybel28 :::"xi"::: ) (Set (Var "L"))))) "holds" (Bool (Set (Var "U1")) "is" ($#v3_waybel11 :::"property(S)"::: ) ))) ; theorem :: WAYBEL28:28 (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 "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L"))))) "holds" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k4_waybel28 :::"xi"::: ) (Set (Var "L")))))) ; theorem :: WAYBEL28:29 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v13_waybel_0 :::"upper"::: ) ) & (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k4_waybel28 :::"xi"::: ) (Set (Var "L"))))) "holds" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")))))) ; theorem :: WAYBEL28:30 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v12_waybel_0 :::"lower"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k4_waybel28 :::"xi"::: ) (Set (Var "L")))) "iff" (Bool (Set (Var "A")) "is" ($#v2_waybel11 :::"closed_under_directed_sups"::: ) ) ")" ))) ;