:: YELLOW_9 semantic presentation begin scheme :: YELLOW_9:sch 1 FraenkelInvolution{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ), F3() -> ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ), F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) } : (Bool (Set F2 "(" ")" ) ($#r1_hidden :::"="::: ) "{" (Set F4 "(" (Set (Var "a")) ")" ) where a "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" )) "}" ) provided (Bool (Set F3 "(" ")" ) ($#r1_hidden :::"="::: ) "{" (Set F4 "(" (Set (Var "a")) ")" ) where a "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) "}" ) and (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set F4 "(" (Set F4 "(" (Set (Var "a")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a")))) proof end; scheme :: YELLOW_9:sch 2 FraenkelComplement1{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) , F2() -> ($#m1_subset_1 :::"Subset-Family":::) "of" (Set F1 "(" ")" ), F3() -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) } : (Bool (Set ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set F2 "(" ")" )) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set F4 "(" (Set (Var "a")) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) where a "is" ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" ) : (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" )) "}" ) provided (Bool (Set F2 "(" ")" ) ($#r1_hidden :::"="::: ) "{" (Set F4 "(" (Set (Var "a")) ")" ) where a "is" ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" ) : (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" )) "}" ) proof end; scheme :: YELLOW_9:sch 3 FraenkelComplement2{ F1() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) , F2() -> ($#m1_subset_1 :::"Subset-Family":::) "of" (Set F1 "(" ")" ), F3() -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) } : (Bool (Set ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set F2 "(" ")" )) ($#r1_hidden :::"="::: ) "{" (Set F4 "(" (Set (Var "a")) ")" ) where a "is" ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" ) : (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" )) "}" ) provided (Bool (Set F2 "(" ")" ) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set F4 "(" (Set (Var "a")) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) where a "is" ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" ) : (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" )) "}" ) proof end; theorem :: YELLOW_9:1 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x")) ")" ) ($#k3_subset_1 :::"`"::: ) )) "iff" (Bool (Bool "not" (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y")))) ")" ))) ; scheme :: YELLOW_9:sch 4 ABC{ F1() -> ($#l1_pre_topc :::"TopSpace":::), F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"Function":::), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool (Set (Set F3 "(" ")" ) ($#k8_relat_1 :::"""::: ) (Set "(" ($#k3_tarski :::"union"::: ) "{" (Set F2 "(" (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "x"))]) "}" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set F3 "(" ")" ) ($#k8_relat_1 :::"""::: ) (Set F2 "(" (Set (Var "y")) ")" ) ")" ) where y "is" ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "y"))]) "}" )) proof end; theorem :: YELLOW_9:2 (Bool "for" (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#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 "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "X")) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set "(" (Set (Var "X")) ($#k3_subset_1 :::"`"::: ) ")" ))))))) ; theorem :: YELLOW_9:3 (Bool "for" (Set (Var "T")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k7_setfam_1 :::"COMPLEMENT"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "a")) ($#k3_subset_1 :::"`"::: ) ")" ) where a "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" ))) ; theorem :: YELLOW_9:4 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" )) & (Bool (Set ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k5_waybel_0 :::"downarrow"::: ) (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" )) ")" ))) ; theorem :: YELLOW_9:5 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set "(" ($#k6_waybel_0 :::"uparrow"::: ) (Set (Var "x")) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" )) "holds" (Bool (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "F")) ")" ) ($#k3_subset_1 :::"`"::: ) ))))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v2_pre_topc :::"correct"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v3_lattice3 :::"complete"::: ) ($#v1_waybel_9 :::"strict"::: ) for ($#l1_waybel_9 :::"TopRelStr"::: ) ; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v2_yellow_0 :::"upper-bounded"::: ) ($#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" "S") ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S")) ($#v1_funct_2 :::"quasi_total"::: ) ($#v17_waybel_0 :::"infs-preserving"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "T" 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 ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S")) ($#v1_funct_2 :::"quasi_total"::: ) ($#v18_waybel_0 :::"sups-preserving"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "R", "S" be ($#l1_struct_0 :::"1-sorted"::: ) ; assume (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "R")))) ; func :::"incl"::: "(" "S" "," "R" ")" -> ($#m1_subset_1 :::"Function":::) "of" "S" "," "R" equals :: YELLOW_9:def 1 (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S")); end; :: deftheorem defines :::"incl"::: YELLOW_9:def 1 : (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#l1_struct_0 :::"1-sorted"::: ) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))))) "holds" (Bool (Set ($#k1_yellow_9 :::"incl"::: ) "(" (Set (Var "S")) "," (Set (Var "R")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))))); registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Const "R")); cluster (Set ($#k1_yellow_9 :::"incl"::: ) "(" "S" "," "R" ")" ) -> ($#v5_orders_3 :::"monotone"::: ) ; end; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "R")); func "X" :::"+id"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_waybel_0 :::"strict"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" "R" equals :: YELLOW_9:def 2 (Set (Set "(" ($#k1_yellow_9 :::"incl"::: ) "(" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) "X" ")" ) "," "R" ")" ")" ) ($#k6_waybel_9 :::"*"::: ) (Set "(" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) "X" ")" ) ($#k2_waybel_9 :::"+id"::: ) ")" )); func "X" :::"opp+id"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_waybel_0 :::"strict"::: ) ($#l1_waybel_0 :::"NetStr"::: ) "over" "R" equals :: YELLOW_9:def 3 (Set (Set "(" ($#k1_yellow_9 :::"incl"::: ) "(" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) "X" ")" ) "," "R" ")" ")" ) ($#k6_waybel_9 :::"*"::: ) (Set "(" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) "X" ")" ) ($#k3_waybel_9 :::"opp+id"::: ) ")" )); end; :: deftheorem defines :::"+id"::: YELLOW_9:def 2 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool (Set (Set (Var "X")) ($#k2_yellow_9 :::"+id"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_yellow_9 :::"incl"::: ) "(" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "X")) ")" ) "," (Set (Var "R")) ")" ")" ) ($#k6_waybel_9 :::"*"::: ) (Set "(" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "X")) ")" ) ($#k2_waybel_9 :::"+id"::: ) ")" ))))); :: deftheorem defines :::"opp+id"::: YELLOW_9:def 3 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool (Set (Set (Var "X")) ($#k3_yellow_9 :::"opp+id"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_yellow_9 :::"incl"::: ) "(" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "X")) ")" ) "," (Set (Var "R")) ")" ")" ) ($#k6_waybel_9 :::"*"::: ) (Set "(" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "X")) ")" ) ($#k3_waybel_9 :::"opp+id"::: ) ")" ))))); theorem :: YELLOW_9:6 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "X")) ($#k2_yellow_9 :::"+id"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "X")) ($#k2_yellow_9 :::"+id"::: ) ) "is" ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Var "R"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "X")) ($#k2_yellow_9 :::"+id"::: ) ")" ) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k2_yellow_9 :::"+id"::: ) ")" ) ($#k2_waybel_0 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ) ")" ))) ; theorem :: YELLOW_9:7 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "X")) ($#k3_yellow_9 :::"opp+id"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "X")) ($#k3_yellow_9 :::"opp+id"::: ) ) "is" ($#v4_yellow_0 :::"full"::: ) ($#m1_yellow_0 :::"SubRelStr"::: ) "of" (Set (Set (Var "R")) ($#k7_lattice3 :::"opp"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "X")) ($#k3_yellow_9 :::"opp+id"::: ) ")" ) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k3_yellow_9 :::"opp+id"::: ) ")" ) ($#k2_waybel_0 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ) ")" ))) ; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "R")); cluster (Set "X" ($#k2_yellow_9 :::"+id"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v6_waybel_0 :::"strict"::: ) ; cluster (Set "X" ($#k3_yellow_9 :::"opp+id"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v6_waybel_0 :::"strict"::: ) ; end; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "R")); cluster (Set "X" ($#k2_yellow_9 :::"+id"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#v6_waybel_0 :::"strict"::: ) ; cluster (Set "X" ($#k3_yellow_9 :::"opp+id"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#v6_waybel_0 :::"strict"::: ) ; end; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "I" be ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "R")); cluster (Set ($#k5_yellow_0 :::"subrelstr"::: ) "I") -> ($#v7_waybel_0 :::"directed"::: ) ; end; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_waybel_0 :::"directed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "R")); cluster (Set "I" ($#k2_yellow_9 :::"+id"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_waybel_0 :::"strict"::: ) ($#v7_waybel_0 :::"directed"::: ) ; end; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_waybel_0 :::"filtered"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "R")); cluster (Set (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) "F" ")" ) ($#k3_waybel_9 :::"opp+id"::: ) ) -> ($#v7_waybel_0 :::"directed"::: ) ; end; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_waybel_0 :::"filtered"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "R")); cluster (Set "F" ($#k3_yellow_9 :::"opp+id"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_waybel_0 :::"strict"::: ) ($#v7_waybel_0 :::"directed"::: ) ; end; begin theorem :: YELLOW_9:8 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "T")) "is" ($#v2_struct_0 :::"empty"::: ) )) "holds" (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: YELLOW_9:9 (Bool "for" (Set (Var "T")) "being" (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k2_tarski :::"}"::: ) )) ")" ) ")" ) ")" )) ; theorem :: YELLOW_9:10 (Bool "for" (Set (Var "T")) "being" (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ($#k1_tarski :::"}"::: ) ) "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T"))) & (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) "is" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T"))) & (Bool (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) "is" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T"))) ")" )) ; theorem :: YELLOW_9:11 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "Y")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k2_cantor_1 :::"FinMeetCl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_tarski :::"}"::: ) )) & (Bool (Set ($#k1_cantor_1 :::"UniCl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "Y")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k2_tarski :::"}"::: ) )) ")" ))) ; theorem :: YELLOW_9:12 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) ))) "or" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) ))) ")" )) "holds" (Bool (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "B")))))) ; theorem :: YELLOW_9:13 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) ))) "or" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) ))) ")" )) "holds" (Bool (Set ($#k2_cantor_1 :::"FinMeetCl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_cantor_1 :::"FinMeetCl"::: ) (Set (Var "B")))))) ; theorem :: YELLOW_9:14 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cantor_1 :::"FinMeetCl"::: ) (Set (Var "A")))) "iff" (Bool "ex" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "Y")))) ")" )) ")" )))) ; theorem :: YELLOW_9:15 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_cantor_1 :::"UniCl"::: ) (Set "(" ($#k1_cantor_1 :::"UniCl"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_cantor_1 :::"UniCl"::: ) (Set (Var "A")))))) ; theorem :: YELLOW_9:16 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v1_xboole_0 :::"empty"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_cantor_1 :::"UniCl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: YELLOW_9:17 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v1_xboole_0 :::"empty"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k2_cantor_1 :::"FinMeetCl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: YELLOW_9:18 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "X")) ($#k2_tarski :::"}"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k1_cantor_1 :::"UniCl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set ($#k2_cantor_1 :::"FinMeetCl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" ))) ; theorem :: YELLOW_9:19 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "implies" (Bool (Set ($#k1_cantor_1 :::"UniCl"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_cantor_1 :::"UniCl"::: ) (Set (Var "B")))) ")" & "(" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B")))) "implies" (Bool (Set ($#k1_cantor_1 :::"UniCl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_cantor_1 :::"UniCl"::: ) (Set (Var "B")))) ")" ")" )))) ; theorem :: YELLOW_9:20 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k2_cantor_1 :::"FinMeetCl"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_tarski :::"{"::: ) (Set (Var "Y")) ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k2_cantor_1 :::"FinMeetCl"::: ) (Set (Var "A")) ")" )))))) ; theorem :: YELLOW_9:21 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_cantor_1 :::"UniCl"::: ) (Set "(" ($#k2_cantor_1 :::"FinMeetCl"::: ) (Set "(" ($#k1_cantor_1 :::"UniCl"::: ) (Set (Var "A")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_cantor_1 :::"UniCl"::: ) (Set "(" ($#k2_cantor_1 :::"FinMeetCl"::: ) (Set (Var "A")) ")" ))))) ; begin theorem :: YELLOW_9:22 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k1_cantor_1 :::"UniCl"::: ) (Set (Var "K")))) "iff" (Bool (Set (Var "K")) "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T"))) ")" ))) ; theorem :: YELLOW_9:23 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "K")) "is" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T"))) "iff" (Bool (Set ($#k2_cantor_1 :::"FinMeetCl"::: ) (Set (Var "K"))) "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T"))) ")" ))) ; theorem :: YELLOW_9:24 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set ($#k1_cantor_1 :::"UniCl"::: ) (Set (Var "B"))) "is" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T")))) "holds" (Bool (Set (Var "B")) "is" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T"))))) ; theorem :: YELLOW_9:25 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T1")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T2")))) & (Bool (Set (Var "B")) "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T2")))) "holds" (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T2")))))) ; theorem :: YELLOW_9:26 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T1")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T2")))) & (Bool (Set (Var "P")) "is" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T2")))) "holds" (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T2")))))) ; theorem :: YELLOW_9:27 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "K")) "is" ($#v1_tops_2 :::"open"::: ) ) & (Bool (Set (Var "K")) "is" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T"))) ")" ))) ; theorem :: YELLOW_9:28 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T")) "holds" (Bool (Set (Var "K")) "is" ($#v1_tops_2 :::"open"::: ) ))) ; theorem :: YELLOW_9:29 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "B")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ($#k1_tarski :::"}"::: ) )) "is" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T"))))) ; theorem :: YELLOW_9:30 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "B")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ($#k1_tarski :::"}"::: ) )) "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T"))))) ; theorem :: YELLOW_9:31 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) ")" ))) ")" )))) ; theorem :: YELLOW_9:32 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T")))) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) ")" ))) ")" )) "holds" (Bool (Set (Var "B")) "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T"))))) ; theorem :: YELLOW_9:33 (Bool "for" (Set (Var "S")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")) (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_pre_topc :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "K")))) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" )) "is" ($#v4_pre_topc :::"closed"::: ) )) ")" ))))) ; theorem :: YELLOW_9:34 (Bool "for" (Set (Var "S")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")) (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_pre_topc :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "K")))) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "A"))) "is" ($#v3_pre_topc :::"open"::: ) )) ")" ))))) ; theorem :: YELLOW_9:35 (Bool "for" (Set (Var "S")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T")) (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_pre_topc :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "K")))) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" )) "is" ($#v4_pre_topc :::"closed"::: ) )) ")" ))))) ; theorem :: YELLOW_9:36 (Bool "for" (Set (Var "S")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T")) (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_pre_topc :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "K")))) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "A"))) "is" ($#v3_pre_topc :::"open"::: ) )) ")" ))))) ; theorem :: YELLOW_9:37 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")) "st" (Bool (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "A")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "X"))) ")" )) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "X")))))))) ; theorem :: YELLOW_9:38 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T")) "st" (Bool (Bool "(" "for" (Set (Var "Z")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set (Var "K"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "Z"))))) "holds" (Bool (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "Z"))) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "X"))) ")" )) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "X")))))))) ; theorem :: YELLOW_9:39 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "N")) "being" ($#l1_waybel_0 :::"net":::) "of" (Set (Var "T")) "st" (Bool (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "K"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "N")) ($#r1_waybel_0 :::"is_eventually_in"::: ) (Set (Var "A"))) ")" )) "holds" (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k1_waybel_0 :::"netmap"::: ) "(" (Set (Var "N")) "," (Set (Var "T")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "S"))))))))) ; begin theorem :: YELLOW_9:40 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B1")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T1")) (Bool "for" (Set (Var "B2")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T2")) "holds" (Bool "{" (Set ($#k3_borsuk_1 :::"[:"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_borsuk_1 :::":]"::: ) ) where a "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T1")), b "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T2")) : (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "B1"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B2"))) ")" ) "}" "is" ($#m1_subset_1 :::"Basis":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T1")) "," (Set (Var "T2")) ($#k2_borsuk_1 :::":]"::: ) ))))) ; theorem :: YELLOW_9:41 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B1")) "being" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T1")) (Bool "for" (Set (Var "B2")) "being" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T2")) "holds" (Bool (Set "{" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T1"))) "," (Set (Var "b")) ($#k2_zfmisc_1 :::":]"::: ) ) where b "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T2")) : (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B2"))) "}" ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "a")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T2"))) ($#k2_zfmisc_1 :::":]"::: ) ) where a "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T1")) : (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "B1"))) "}" ) "is" ($#m1_subset_1 :::"prebasis":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T1")) "," (Set (Var "T2")) ($#k2_borsuk_1 :::":]"::: ) ))))) ; theorem :: YELLOW_9:42 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "A1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "A2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X2")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) "{" (Set ($#k8_mcart_1 :::"[:"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k8_mcart_1 :::":]"::: ) ) where a "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")), b "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X2")) : (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A1"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A2"))) ")" ) "}" )) "holds" (Bool (Set ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "A"))) ($#r2_relset_1 :::"="::: ) (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "A1")) ")" ) "," (Set "(" ($#k8_setfam_1 :::"Intersect"::: ) (Set (Var "A2")) ")" ) ($#k8_mcart_1 :::":]"::: ) )))))) ; theorem :: YELLOW_9:43 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B1")) "being" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T1")) (Bool "for" (Set (Var "B2")) "being" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T2")) "st" (Bool (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "B1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T1")))) & (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "B2"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T2"))))) "holds" (Bool "{" (Set ($#k3_borsuk_1 :::"[:"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_borsuk_1 :::":]"::: ) ) where a "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T1")), b "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T2")) : (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "B1"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B2"))) ")" ) "}" "is" ($#m1_subset_1 :::"prebasis":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T1")) "," (Set (Var "T2")) ($#k2_borsuk_1 :::":]"::: ) ))))) ; begin definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; mode :::"TopAugmentation"::: "of" "R" -> ($#l1_waybel_9 :::"TopRelStr"::: ) means :: YELLOW_9:def 4 (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" "R") "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "R") "#)" )); end; :: deftheorem defines :::"TopAugmentation"::: YELLOW_9:def 4 : (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#l1_waybel_9 :::"TopRelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "R"))) "iff" (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 "R"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) "#)" )) ")" ))); notationlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; let "T" be ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Const "R")); synonym :::"correct"::: "T" for :::"TopSpace-like"::: ; end; registrationlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v2_pre_topc :::"correct"::: ) ($#v1_tdlat_3 :::"discrete"::: ) ($#v1_waybel_9 :::"strict"::: ) for ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" "R"; end; theorem :: YELLOW_9:44 (Bool "for" (Set (Var "T")) "being" ($#l1_waybel_9 :::"TopRelStr"::: ) "holds" (Bool (Set (Var "T")) "is" ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "T")))) ; theorem :: YELLOW_9:45 (Bool "for" (Set (Var "S")) "being" ($#l1_waybel_9 :::"TopRelStr"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "S")) "holds" (Bool (Set (Var "S")) "is" ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "T"))))) ; theorem :: YELLOW_9:46 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "T1")) "being" ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "R")) (Bool "for" (Set (Var "T2")) "being" ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "T1")) "holds" (Bool (Set (Var "T2")) "is" ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "R")))))) ; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" "R"; end; registrationlet "R" be ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster -> ($#v3_orders_2 :::"reflexive"::: ) for ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" "R"; end; registrationlet "R" be ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster -> ($#v4_orders_2 :::"transitive"::: ) for ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" "R"; end; registrationlet "R" be ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster -> ($#v5_orders_2 :::"antisymmetric"::: ) for ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" "R"; end; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster -> ($#v3_lattice3 :::"complete"::: ) for ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" "R"; end; theorem :: YELLOW_9:47 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v24_waybel_0 :::"up-complete"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) "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 "T"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T"))) "#)" ))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) "is" ($#v1_waybel11 :::"inaccessible"::: ) )) "holds" (Bool (Set (Var "C")) "is" ($#v1_waybel11 :::"inaccessible"::: ) ))))) ; theorem :: YELLOW_9:48 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k5_waybel11 :::"sigma"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Var "T")) "is" ($#v2_pre_topc :::"correct"::: ) ))) ; theorem :: YELLOW_9:49 (Bool "for" (Set (Var "S")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "T")) "being" ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k5_waybel11 :::"sigma"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Var "T")) "is" ($#v4_waybel11 :::"Scott"::: ) ))) ; registrationlet "R" be ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"correct"::: ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_lattice3 :::"with_suprema"::: ) ($#v2_lattice3 :::"with_infima"::: ) ($#v3_lattice3 :::"complete"::: ) ($#v1_yellow_0 :::"lower-bounded"::: ) ($#v2_yellow_0 :::"upper-bounded"::: ) bbbadV3_YELLOW_0() ($#v24_waybel_0 :::"up-complete"::: ) ($#v25_waybel_0 :::"/\-complete"::: ) ($#v1_waybel_9 :::"strict"::: ) ($#v4_waybel11 :::"Scott"::: ) for ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" "R"; end; theorem :: YELLOW_9:50 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_lattice3 :::"complete"::: ) ($#v4_waybel11 :::"Scott"::: ) ($#l1_waybel_9 :::"TopRelStr"::: ) "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 "T"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T"))) "#)" ))) "holds" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "G"))) & (Bool (Set (Var "F")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) )))) ; theorem :: YELLOW_9:51 (Bool "for" (Set (Var "S")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) (Bool "for" (Set (Var "T")) "being" ($#v4_waybel11 :::"Scott"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "S")) "holds" (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k5_waybel11 :::"sigma"::: ) (Set (Var "S")))))) ; theorem :: YELLOW_9:52 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::) "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 "T"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T"))) "#)" ))) "holds" (Bool (Set ($#k5_waybel11 :::"sigma"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k5_waybel11 :::"sigma"::: ) (Set (Var "T"))))) ; registrationlet "R" be ($#v3_lattice3 :::"complete"::: ) ($#l1_orders_2 :::"LATTICE":::); cluster ($#v4_waybel11 :::"Scott"::: ) -> ($#v2_pre_topc :::"correct"::: ) for ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" "R"; end; begin definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; mode :::"TopExtension"::: "of" "T" -> ($#l1_pre_topc :::"TopSpace":::) means :: YELLOW_9:def 5 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it)) & (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "T") ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" it)) ")" ); end; :: deftheorem defines :::"TopExtension"::: YELLOW_9:def 5 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "b2")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_yellow_9 :::"TopExtension"::: ) "of" (Set (Var "T"))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2")))) & (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "b2")))) ")" ) ")" ))); theorem :: YELLOW_9:53 (Bool "for" (Set (Var "S")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "ex" (Set (Var "T")) "being" ($#m2_yellow_9 :::"TopExtension"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "T")) "is" ($#v1_pre_topc :::"strict"::: ) ) & (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "S"))) "is" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T"))) ")" ))) ; registrationlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"correct"::: ) ($#v1_tdlat_3 :::"discrete"::: ) for ($#m2_yellow_9 :::"TopExtension"::: ) "of" "T"; end; definitionlet "T1", "T2" be ($#l1_pre_topc :::"TopStruct"::: ) ; mode :::"Refinement"::: "of" "T1" "," "T2" -> ($#l1_pre_topc :::"TopSpace":::) means :: YELLOW_9:def 6 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T1") ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T2"))) & (Bool (Set (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "T1") ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "T2")) "is" ($#m1_subset_1 :::"prebasis":::) "of" it) ")" ); end; :: deftheorem defines :::"Refinement"::: YELLOW_9:def 6 : (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "b3")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m3_yellow_9 :::"Refinement"::: ) "of" (Set (Var "T1")) "," (Set (Var "T2"))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T1"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T2"))))) & (Bool (Set (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T1"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T2")))) "is" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "b3"))) ")" ) ")" ))); registrationlet "T1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "T2" be ($#l1_pre_topc :::"TopStruct"::: ) ; cluster -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#m3_yellow_9 :::"Refinement"::: ) "of" "T1" "," "T2"; cluster -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#m3_yellow_9 :::"Refinement"::: ) "of" "T2" "," "T1"; end; theorem :: YELLOW_9:54 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "T")) "," (Set (Var "T9")) "being" ($#m3_yellow_9 :::"Refinement"::: ) "of" (Set (Var "T1")) "," (Set (Var "T2")) "holds" (Bool (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"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T9"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T9"))) "#)" )))) ; theorem :: YELLOW_9:55 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "T")) "being" ($#m3_yellow_9 :::"Refinement"::: ) "of" (Set (Var "T1")) "," (Set (Var "T2")) "holds" (Bool (Set (Var "T")) "is" ($#m3_yellow_9 :::"Refinement"::: ) "of" (Set (Var "T2")) "," (Set (Var "T1"))))) ; theorem :: YELLOW_9:56 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "T")) "being" ($#m3_yellow_9 :::"Refinement"::: ) "of" (Set (Var "T1")) "," (Set (Var "T2")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T1"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T2")))))) "holds" (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k1_cantor_1 :::"UniCl"::: ) (Set "(" ($#k2_cantor_1 :::"FinMeetCl"::: ) (Set (Var "X")) ")" )))))) ; theorem :: YELLOW_9:57 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T2"))))) "holds" (Bool "for" (Set (Var "T")) "being" ($#m3_yellow_9 :::"Refinement"::: ) "of" (Set (Var "T1")) "," (Set (Var "T2")) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#m2_yellow_9 :::"TopExtension"::: ) "of" (Set (Var "T1"))) & (Bool (Set (Var "T")) "is" ($#m2_yellow_9 :::"TopExtension"::: ) "of" (Set (Var "T2"))) ")" ))) ; theorem :: YELLOW_9:58 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "T")) "being" ($#m3_yellow_9 :::"Refinement"::: ) "of" (Set (Var "T1")) "," (Set (Var "T2")) (Bool "for" (Set (Var "B1")) "being" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T1")) (Bool "for" (Set (Var "B2")) "being" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T2")) "holds" (Bool (Set (Set "(" (Set (Var "B1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B2")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T1"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T2"))) ($#k2_tarski :::"}"::: ) )) "is" ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T"))))))) ; theorem :: YELLOW_9:59 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B1")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T1")) (Bool "for" (Set (Var "B2")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T2")) (Bool "for" (Set (Var "T")) "being" ($#m3_yellow_9 :::"Refinement"::: ) "of" (Set (Var "T1")) "," (Set (Var "T2")) "holds" (Bool (Set (Set "(" (Set (Var "B1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B2")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k3_setfam_1 :::"INTERSECTION"::: ) "(" (Set (Var "B1")) "," (Set (Var "B2")) ")" ")" )) "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T"))))))) ; theorem :: YELLOW_9:60 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T2"))))) "holds" (Bool "for" (Set (Var "T")) "being" ($#m3_yellow_9 :::"Refinement"::: ) "of" (Set (Var "T1")) "," (Set (Var "T2")) "holds" (Bool (Set ($#k3_setfam_1 :::"INTERSECTION"::: ) "(" (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T2"))) ")" ) "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T"))))) ; theorem :: YELLOW_9:61 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#v2_pre_topc :::"correct"::: ) ($#m1_yellow_9 :::"TopAugmentation"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "T")) "being" ($#m3_yellow_9 :::"Refinement"::: ) "of" (Set (Var "T1")) "," (Set (Var "T2")) "holds" (Bool (Set ($#k3_setfam_1 :::"INTERSECTION"::: ) "(" (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T2"))) ")" ) "is" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")))))) ;