:: WAYBEL29 semantic presentation begin theorem :: WAYBEL29:1 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Z")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Set (Var "Z")) ($#k6_yellow_1 :::"|^"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Set "(" (Set (Var "Z")) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "Y")) ")" ) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_waybel27 :::"currying"::: ) ) & (Bool (Set (Var "f")) "is" bbbadV2_FUNCT_1()) & (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k2_tops_2 :::"""::: ) ) "is" ($#v1_waybel27 :::"uncurrying"::: ) )))))) ; theorem :: WAYBEL29:2 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Z")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Set (Var "Z")) ($#k6_yellow_1 :::"|^"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Set "(" (Set (Var "Z")) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "Y")) ")" ) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_waybel27 :::"uncurrying"::: ) ) & (Bool (Set (Var "f")) "is" bbbadV2_FUNCT_1()) & (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k2_tops_2 :::"""::: ) ) "is" ($#v2_waybel27 :::"currying"::: ) )))))) ; theorem :: WAYBEL29:3 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Z")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Set (Var "Z")) ($#k6_yellow_1 :::"|^"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Set "(" (Set (Var "Z")) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "Y")) ")" ) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_waybel27 :::"currying"::: ) ) & (Bool (Set (Var "f")) "is" bbbadV2_FUNCT_1()) & (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) )))))) ; theorem :: WAYBEL29:4 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Z")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Set (Var "Z")) ($#k6_yellow_1 :::"|^"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Set "(" (Set (Var "Z")) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "Y")) ")" ) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_waybel27 :::"uncurrying"::: ) ) & (Bool (Set (Var "f")) "is" bbbadV2_FUNCT_1()) & (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) )))))) ; theorem :: WAYBEL29:5 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#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 "S2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "S2"))) "#)" )) & (Bool (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"))) "#)" ) ($#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 "T1")) "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 "S2")) "," (Set (Var "T2")) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "f")))) "holds" (Bool (Set (Var "g")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) )))) ; theorem :: WAYBEL29:6 (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "R")) "," (Set (Var "S")) "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 "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "g")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) )) "holds" (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "R")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "h")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "h")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) ))))) ; theorem :: WAYBEL29:7 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "X1")) "," (Set (Var "Y1")) "being" ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X1"))) "#)" )) & (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y1"))) "#)" ))) "holds" (Bool (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_borsuk_1 :::":]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "Y1")) ($#k2_borsuk_1 :::":]"::: ) ))) ; theorem :: WAYBEL29:8 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopPoset":::) (Bool "for" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_waybel24 :::"ContMaps"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ")" ) "holds" (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set (Var "F")) "," (Set "(" (Set (Var "L")) ($#k6_yellow_1 :::"|^"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) ")" ) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "L")))))) ; theorem :: WAYBEL29:9 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopPoset":::) "holds" (Bool (Set ($#k3_waybel24 :::"ContMaps"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ) "is" ($#v4_waybel_0 :::"directed-sups-inheriting"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Set (Var "L")) ($#k6_yellow_1 :::"|^"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))))))) ; theorem :: WAYBEL29:10 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "st" (Bool (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "S1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "S2"))) "#)" ))) "holds" (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_waybel_9 :::"TopRelStr"::: ) "st" (Bool (Bool (Set ($#g1_waybel_9 :::"TopRelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_waybel_9 :::"TopRelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T2"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T2"))) "#)" ))) "holds" (Bool (Set ($#k3_waybel24 :::"ContMaps"::: ) "(" (Set (Var "S1")) "," (Set (Var "T1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_waybel24 :::"ContMaps"::: ) "(" (Set (Var "S2")) "," (Set (Var "T2")) ")" )))) ; registration cluster ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v3_lattice3 :::"complete"::: ) -> ($#v6_pre_topc :::"T_0"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#v2_waybel18 :::"injective"::: ) ($#v3_lattice3 :::"complete"::: ) for ($#l1_waybel_9 :::"TopRelStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#~v1_yellow_3 "non" ($#v1_yellow_3 :::"void"::: ) ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v3_lattice3 :::"complete"::: ) for ($#l1_waybel_9 :::"TopRelStr"::: ) ; end; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopPoset":::); cluster (Set ($#k3_waybel24 :::"ContMaps"::: ) "(" "X" "," "L" ")" ) -> ($#v24_waybel_0 :::"up-complete"::: ) ; end; theorem :: WAYBEL29:11 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#v4_waybel_3 :::"non-Empty"::: ) ($#v1_yellow16 :::"Poset-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "J")) ($#k2_yellow16 :::"."::: ) (Set (Var "i"))) "is" ($#v24_waybel_0 :::"up-complete"::: ) ) ")" )) "holds" (Bool (Set (Set (Var "I")) ($#k5_yellow_1 :::"-POS_prod"::: ) (Set (Var "J"))) "is" ($#v24_waybel_0 :::"up-complete"::: ) ))) ; theorem :: WAYBEL29:12 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#v4_waybel_3 :::"non-Empty"::: ) ($#v1_yellow16 :::"Poset-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Set (Var "J")) ($#k2_yellow16 :::"."::: ) (Set (Var "i"))) "is" ($#v24_waybel_0 :::"up-complete"::: ) ) & (Bool (Set (Set (Var "J")) ($#k2_yellow16 :::"."::: ) (Set (Var "i"))) "is" ($#v1_yellow_0 :::"lower-bounded"::: ) ) ")" ) ")" )) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_yellow_1 :::"product"::: ) (Set (Var "J")) ")" ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_waybel_3 :::"<<"::: ) (Set (Var "y"))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "x")) ($#k4_waybel_3 :::"."::: ) (Set (Var "i"))) ($#r1_waybel_3 :::"<<"::: ) (Set (Set (Var "y")) ($#k4_waybel_3 :::"."::: ) (Set (Var "i")))) ")" ) & (Bool "ex" (Set (Var "K")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "I")) "st" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "st" (Bool (Bool (Bool "not" (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))))) "holds" (Bool (Set (Set (Var "x")) ($#k4_waybel_3 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k3_yellow_0 :::"Bottom"::: ) (Set "(" (Set (Var "J")) ($#k2_yellow16 :::"."::: ) (Set (Var "i")) ")" ))))) ")" ) ")" )))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "L" ($#k6_yellow_1 :::"|^"::: ) "X") -> ($#v1_yellow_0 :::"lower-bounded"::: ) ; end; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#l1_waybel_9 :::"TopPoset":::); cluster (Set ($#k3_waybel24 :::"ContMaps"::: ) "(" "X" "," "L" ")" ) -> ($#v1_yellow_0 :::"lower-bounded"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"Poset":::); cluster -> ($#v24_waybel_0 :::"up-complete"::: ) for ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" "L"; cluster ($#v4_waybel11 :::"Scott"::: ) -> ($#v2_pre_topc :::"correct"::: ) for ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" "L"; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"Poset":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v24_waybel_0 :::"up-complete"::: ) ($#v1_waybel_9 :::"strict"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#~v1_yellow_3 "non" ($#v1_yellow_3 :::"void"::: ) ) for ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" "L"; end; theorem :: WAYBEL29:13 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "L")) "holds" (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "S1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "S2")))))) ; theorem :: WAYBEL29:14 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_waybel_9 :::"TopRelStr"::: ) "st" (Bool (Bool (Set ($#g1_waybel_9 :::"TopRelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "S1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "S1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_waybel_9 :::"TopRelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "S2"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "S2"))) "#)" )) & (Bool (Set (Var "S1")) "is" ($#v4_waybel11 :::"Scott"::: ) )) "holds" (Bool (Set (Var "S2")) "is" ($#v4_waybel11 :::"Scott"::: ) )) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"Poset":::); func :::"Sigma"::: "L" -> ($#v1_waybel_9 :::"strict"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" "L" means :: WAYBEL29:def 1 (Bool verum); end; :: deftheorem defines :::"Sigma"::: WAYBEL29:def 1 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "b2")) "being" ($#v1_waybel_9 :::"strict"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel29 :::"Sigma"::: ) (Set (Var "L")))) "iff" (Bool verum) ")" ))); theorem :: WAYBEL29:15 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopPoset":::) "holds" (Bool (Set ($#k1_waybel29 :::"Sigma"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#g1_waybel_9 :::"TopRelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "S"))) "#)" ))) ; theorem :: WAYBEL29:16 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"Poset":::) "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 (Set ($#k1_waybel29 :::"Sigma"::: ) (Set (Var "L1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel29 :::"Sigma"::: ) (Set (Var "L2"))))) ; definitionlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"Poset":::); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); func :::"Sigma"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_waybel29 :::"Sigma"::: ) "S" ")" ) "," (Set "(" ($#k1_waybel29 :::"Sigma"::: ) "T" ")" ) equals :: WAYBEL29:def 2 "f"; end; :: deftheorem defines :::"Sigma"::: WAYBEL29:def 2 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "holds" (Bool (Set ($#k2_waybel29 :::"Sigma"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f"))))); registrationlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"Poset":::); let "f" be ($#v22_waybel_0 :::"directed-sups-preserving"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); cluster (Set ($#k2_waybel29 :::"Sigma"::: ) "f") -> ($#v5_pre_topc :::"continuous"::: ) ; end; theorem :: WAYBEL29:17 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"Poset":::) (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 (Set ($#k2_waybel29 :::"Sigma"::: ) (Set (Var "f"))) "is" ($#v23_waybel_0 :::"isomorphic"::: ) ) ")" ))) ; theorem :: WAYBEL29:18 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "S")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#v3_lattice3 :::"complete"::: ) ($#l1_waybel_9 :::"TopLattice":::) "holds" (Bool (Set ($#k1_waybel26 :::"oContMaps"::: ) "(" (Set (Var "X")) "," (Set (Var "S")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_waybel24 :::"ContMaps"::: ) "(" (Set (Var "X")) "," (Set (Var "S")) ")" )))) ; definitionlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); func :::"Theta"::: "(" "X" "," "Y" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) "X" "," "Y" ($#k2_borsuk_1 :::":]"::: ) )) ")" ) "," (Set "(" ($#k3_waybel24 :::"ContMaps"::: ) "(" "X" "," (Set "(" ($#k1_waybel29 :::"Sigma"::: ) (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "Y") ")" ) ")" ) ")" ")" ) means :: WAYBEL29:def 3 (Bool "for" (Set (Var "W")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) "X" "," "Y" ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "W")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ")" ($#k6_waybel26 :::"*graph"::: ) ))); end; :: deftheorem defines :::"Theta"::: WAYBEL29:def 3 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_borsuk_1 :::":]"::: ) )) ")" ) "," (Set "(" ($#k3_waybel24 :::"ContMaps"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k1_waybel29 :::"Sigma"::: ) (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y"))) ")" ) ")" ) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_waybel29 :::"Theta"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) "iff" (Bool "for" (Set (Var "W")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "W")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ($#k6_waybel26 :::"*graph"::: ) ))) ")" ))); begin definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); func :::"alpha"::: "X" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_waybel26 :::"oContMaps"::: ) "(" "X" "," (Set ($#k9_waybel18 :::"Sierpinski_Space"::: ) ) ")" ")" ) "," (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "X") ")" ) means :: WAYBEL29:def 4 (Bool "for" (Set (Var "g")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" "X" "," (Set ($#k9_waybel18 :::"Sierpinski_Space"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) )))); end; :: deftheorem defines :::"alpha"::: WAYBEL29:def 4 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_waybel26 :::"oContMaps"::: ) "(" (Set (Var "X")) "," (Set ($#k9_waybel18 :::"Sierpinski_Space"::: ) ) ")" ")" ) "," (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X"))) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_waybel29 :::"alpha"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "g")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k9_waybel18 :::"Sierpinski_Space"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) )))) ")" ))); theorem :: WAYBEL29:19 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "V")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set "(" ($#k4_waybel29 :::"alpha"::: ) (Set (Var "X")) ")" ) ($#k2_tops_2 :::"""::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#k5_funct_3 :::"chi"::: ) "(" (Set (Var "V")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" )))) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k4_waybel29 :::"alpha"::: ) "X") -> ($#v23_waybel_0 :::"isomorphic"::: ) ; end; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster (Set (Set "(" ($#k4_waybel29 :::"alpha"::: ) "X" ")" ) ($#k2_tops_2 :::"""::: ) ) -> ($#v23_waybel_0 :::"isomorphic"::: ) ; end; registrationlet "S" be ($#v2_waybel18 :::"injective"::: ) ($#l1_pre_topc :::"T_0-TopSpace":::); cluster (Set ($#k1_waybel25 :::"Omega"::: ) "S") -> ($#v4_waybel11 :::"Scott"::: ) ; end; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k1_waybel26 :::"oContMaps"::: ) "(" "X" "," (Set ($#k9_waybel18 :::"Sierpinski_Space"::: ) ) ")" ) -> ($#v3_lattice3 :::"complete"::: ) ; end; theorem :: WAYBEL29:20 (Bool (Set ($#k1_waybel25 :::"Omega"::: ) (Set ($#k9_waybel18 :::"Sierpinski_Space"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel29 :::"Sigma"::: ) (Set "(" ($#k3_yellow_1 :::"BoolePoset"::: ) (Num 1) ")" ))) ; registrationlet "M" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#v2_waybel18 :::"injective"::: ) ($#l1_pre_topc :::"T_0-TopSpace":::); cluster (Set ($#k3_waybel18 :::"product"::: ) (Set "(" "M" ($#k2_funcop_1 :::"=>"::: ) "S" ")" )) -> ($#v2_waybel18 :::"injective"::: ) ; end; theorem :: WAYBEL29:21 (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#v3_waybel_3 :::"continuous"::: ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool (Set ($#k1_waybel25 :::"Omega"::: ) (Set "(" (Set (Var "M")) ($#k3_waybel18 :::"-TOP_prod"::: ) (Set "(" (Set (Var "M")) ($#k2_funcop_1 :::"=>"::: ) (Set "(" ($#k1_waybel29 :::"Sigma"::: ) (Set (Var "L")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel29 :::"Sigma"::: ) (Set "(" (Set (Var "M")) ($#k5_yellow_1 :::"-POS_prod"::: ) (Set "(" (Set (Var "M")) ($#k2_funcop_1 :::"=>"::: ) (Set (Var "L")) ")" ) ")" ))))) ; theorem :: WAYBEL29:22 (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "T")) "being" ($#v2_waybel18 :::"injective"::: ) ($#l1_pre_topc :::"T_0-TopSpace":::) "holds" (Bool (Set ($#k1_waybel25 :::"Omega"::: ) (Set "(" (Set (Var "M")) ($#k3_waybel18 :::"-TOP_prod"::: ) (Set "(" (Set (Var "M")) ($#k2_funcop_1 :::"=>"::: ) (Set (Var "T")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel29 :::"Sigma"::: ) (Set "(" (Set (Var "M")) ($#k5_yellow_1 :::"-POS_prod"::: ) (Set "(" (Set (Var "M")) ($#k2_funcop_1 :::"=>"::: ) (Set "(" ($#k1_waybel25 :::"Omega"::: ) (Set (Var "T")) ")" ) ")" ) ")" ))))) ; definitionlet "M" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); func :::"commute"::: "(" "X" "," "M" "," "Y" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_waybel26 :::"oContMaps"::: ) "(" "X" "," (Set "(" "M" ($#k3_waybel18 :::"-TOP_prod"::: ) (Set "(" "M" ($#k2_funcop_1 :::"=>"::: ) "Y" ")" ) ")" ) ")" ")" ) "," (Set "(" (Set "(" ($#k1_waybel26 :::"oContMaps"::: ) "(" "X" "," "Y" ")" ")" ) ($#k6_yellow_1 :::"|^"::: ) "M" ")" ) means :: WAYBEL29:def 5 (Bool "for" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" "X" "," (Set "(" "M" ($#k3_waybel18 :::"-TOP_prod"::: ) (Set "(" "M" ($#k2_funcop_1 :::"=>"::: ) "Y" ")" ) ")" ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k10_funct_6 :::"commute"::: ) (Set (Var "f"))))); end; :: deftheorem defines :::"commute"::: WAYBEL29:def 5 : (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_waybel26 :::"oContMaps"::: ) "(" (Set (Var "X")) "," (Set "(" (Set (Var "M")) ($#k3_waybel18 :::"-TOP_prod"::: ) (Set "(" (Set (Var "M")) ($#k2_funcop_1 :::"=>"::: ) (Set (Var "Y")) ")" ) ")" ) ")" ")" ) "," (Set "(" (Set "(" ($#k1_waybel26 :::"oContMaps"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ($#k6_yellow_1 :::"|^"::: ) (Set (Var "M")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k5_waybel29 :::"commute"::: ) "(" (Set (Var "X")) "," (Set (Var "M")) "," (Set (Var "Y")) ")" )) "iff" (Bool "for" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" (Set (Var "M")) ($#k3_waybel18 :::"-TOP_prod"::: ) (Set "(" (Set (Var "M")) ($#k2_funcop_1 :::"=>"::: ) (Set (Var "Y")) ")" ) ")" ) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k10_funct_6 :::"commute"::: ) (Set (Var "f"))))) ")" )))); registrationlet "M" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k5_waybel29 :::"commute"::: ) "(" "X" "," "M" "," "Y" ")" ) -> bbbadV2_FUNCT_1() ($#v2_funct_2 :::"onto"::: ) ; end; registrationlet "M" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k5_waybel29 :::"commute"::: ) "(" "X" "," "M" "," (Set ($#k9_waybel18 :::"Sierpinski_Space"::: ) ) ")" ) -> ($#v23_waybel_0 :::"isomorphic"::: ) ; end; theorem :: WAYBEL29:23 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "S")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y")))) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_waybel24 :::"ContMaps"::: ) "(" (Set (Var "X")) "," (Set (Var "S")) ")" ")" ) "st" (Bool (Bool (Set (Var "f1")) ($#r3_orders_2 :::"<="::: ) (Set (Var "f2")))) "holds" (Bool (Set ($#k5_waybel26 :::"*graph"::: ) (Set (Var "f1"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_waybel26 :::"*graph"::: ) (Set (Var "f2"))))))) ; begin theorem :: WAYBEL29:24 (Bool "for" (Set (Var "Y")) "being" ($#l1_pre_topc :::"T_0-TopSpace":::) "holds" (Bool "(" (Bool "(" "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "L")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#v3_lattice3 :::"complete"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "T")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set ($#k3_waybel24 :::"ContMaps"::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" ) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_waybel24 :::"ContMaps"::: ) "(" (Set (Var "X")) "," (Set (Var "T")) ")" ")" ) "," (Set "(" ($#k3_waybel24 :::"ContMaps"::: ) "(" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "L")) ")" ")" )(Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_waybel24 :::"ContMaps"::: ) "(" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "L")) ")" ")" ) "," (Set "(" ($#k3_waybel24 :::"ContMaps"::: ) "(" (Set (Var "X")) "," (Set (Var "T")) ")" ")" ) "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_waybel27 :::"uncurrying"::: ) ) & (Bool (Set (Var "f")) "is" bbbadV2_FUNCT_1()) & (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_waybel27 :::"currying"::: ) ) & (Bool (Set (Var "g")) "is" bbbadV2_FUNCT_1()) & (Bool (Set (Var "g")) "is" ($#v2_funct_2 :::"onto"::: ) ) ")" ))))) ")" ) "iff" (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "L")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#v3_waybel_3 :::"continuous"::: ) ($#v3_lattice3 :::"complete"::: ) ($#l1_waybel_9 :::"TopLattice":::) (Bool "for" (Set (Var "T")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set ($#k3_waybel24 :::"ContMaps"::: ) "(" (Set (Var "Y")) "," (Set (Var "L")) ")" ) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_waybel24 :::"ContMaps"::: ) "(" (Set (Var "X")) "," (Set (Var "T")) ")" ")" ) "," (Set "(" ($#k3_waybel24 :::"ContMaps"::: ) "(" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "L")) ")" ")" )(Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_waybel24 :::"ContMaps"::: ) "(" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "L")) ")" ")" ) "," (Set "(" ($#k3_waybel24 :::"ContMaps"::: ) "(" (Set (Var "X")) "," (Set (Var "T")) ")" ")" ) "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_waybel27 :::"uncurrying"::: ) ) & (Bool (Set (Var "f")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_waybel27 :::"currying"::: ) ) & (Bool (Set (Var "g")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) ) ")" )))))) ")" )) ; theorem :: WAYBEL29:25 (Bool "for" (Set (Var "Y")) "being" ($#l1_pre_topc :::"T_0-TopSpace":::) "holds" (Bool "(" (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y")))) "is" ($#v3_waybel_3 :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k3_waybel29 :::"Theta"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) "is" ($#v23_waybel_0 :::"isomorphic"::: ) )) ")" )) ; theorem :: WAYBEL29:26 (Bool "for" (Set (Var "Y")) "being" ($#l1_pre_topc :::"T_0-TopSpace":::) "holds" (Bool "(" (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y")))) "is" ($#v3_waybel_3 :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k1_waybel29 :::"Sigma"::: ) (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y"))) ")" ) ")" ) "holds" (Bool (Set ($#k5_waybel26 :::"*graph"::: ) (Set (Var "f"))) "is" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_borsuk_1 :::":]"::: ) )))) ")" )) ; theorem :: WAYBEL29:27 (Bool "for" (Set (Var "Y")) "being" ($#l1_pre_topc :::"T_0-TopSpace":::) "holds" (Bool "(" (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y")))) "is" ($#v3_waybel_3 :::"continuous"::: ) ) "iff" (Bool "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "W")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) where W "is" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")), y "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Y")) : (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) "}" "is" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k1_waybel29 :::"Sigma"::: ) (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y"))) ")" ) ")" ) "," (Set (Var "Y")) ($#k2_borsuk_1 :::":]"::: ) )) ")" )) ; theorem :: WAYBEL29:28 (Bool "for" (Set (Var "Y")) "being" ($#l1_pre_topc :::"T_0-TopSpace":::) "holds" (Bool "(" (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y")))) "is" ($#v3_waybel_3 :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "V")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "y")) (Bool "ex" (Set (Var "H")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_waybel29 :::"Sigma"::: ) (Set "(" ($#k2_yellow_1 :::"InclPoset"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y"))) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set (Var "H"))) & (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "H"))) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "y"))) ")" )))) ")" )) ; begin theorem :: WAYBEL29:29 (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "," (Set (Var "R3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "R1")) "," (Set (Var "R3")) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) )) "holds" (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "R2")) "," (Set (Var "R3")) "st" (Bool (Bool (Set (Var "f2")) ($#r1_funct_2 :::"="::: ) (Set (Var "f1"))) & (Bool (Set (Var "f2")) "is" ($#v23_waybel_0 :::"isomorphic"::: ) )) "holds" (Bool (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R1"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R2"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R2"))) "#)" ))))) ; theorem :: WAYBEL29:30 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")) ")" )) "is" ($#v3_waybel_3 :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "S")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool (Set ($#k5_waybel11 :::"sigma"::: ) (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "L")) ($#k3_yellow_3 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k1_waybel29 :::"Sigma"::: ) (Set (Var "S")) ")" ) "," (Set "(" ($#k1_waybel29 :::"Sigma"::: ) (Set (Var "L")) ")" ) ($#k2_borsuk_1 :::":]"::: ) )))) ")" )) ; theorem :: WAYBEL29:31 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool "(" "for" (Set (Var "S")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool (Set ($#k5_waybel11 :::"sigma"::: ) (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "L")) ($#k3_yellow_3 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k1_waybel29 :::"Sigma"::: ) (Set (Var "S")) ")" ) "," (Set "(" ($#k1_waybel29 :::"Sigma"::: ) (Set (Var "L")) ")" ) ($#k2_borsuk_1 :::":]"::: ) ))) ")" ) "iff" (Bool "for" (Set (Var "S")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_waybel29 :::"Sigma"::: ) (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "L")) ($#k3_yellow_3 :::":]"::: ) ) ")" )) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set "(" ($#k1_waybel29 :::"Sigma"::: ) (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "L")) ($#k3_yellow_3 :::":]"::: ) ) ")" )) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k1_waybel29 :::"Sigma"::: ) (Set (Var "S")) ")" ) "," (Set "(" ($#k1_waybel29 :::"Sigma"::: ) (Set (Var "L")) ")" ) ($#k2_borsuk_1 :::":]"::: ) ))) ")" )) ; theorem :: WAYBEL29:32 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool "(" "for" (Set (Var "S")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool (Set ($#k5_waybel11 :::"sigma"::: ) (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "L")) ($#k3_yellow_3 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k1_waybel29 :::"Sigma"::: ) (Set (Var "S")) ")" ) "," (Set "(" ($#k1_waybel29 :::"Sigma"::: ) (Set (Var "L")) ")" ) ($#k2_borsuk_1 :::":]"::: ) ))) ")" ) "iff" (Bool "for" (Set (Var "S")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool (Set ($#k1_waybel29 :::"Sigma"::: ) (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "L")) ($#k3_yellow_3 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel25 :::"Omega"::: ) (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k1_waybel29 :::"Sigma"::: ) (Set (Var "S")) ")" ) "," (Set "(" ($#k1_waybel29 :::"Sigma"::: ) (Set (Var "L")) ")" ) ($#k2_borsuk_1 :::":]"::: ) )))) ")" )) ; theorem :: WAYBEL29:33 (Bool "for" (Set (Var "L")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool "(" (Bool (Set ($#k2_yellow_1 :::"InclPoset"::: ) (Set "(" ($#k5_waybel11 :::"sigma"::: ) (Set (Var "L")) ")" )) "is" ($#v3_waybel_3 :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "S")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "holds" (Bool (Set ($#k1_waybel29 :::"Sigma"::: ) (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "L")) ($#k3_yellow_3 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_waybel25 :::"Omega"::: ) (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k1_waybel29 :::"Sigma"::: ) (Set (Var "S")) ")" ) "," (Set "(" ($#k1_waybel29 :::"Sigma"::: ) (Set (Var "L")) ")" ) ($#k2_borsuk_1 :::":]"::: ) )))) ")" )) ;