:: URYSOHN1 semantic presentation begin definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"dyadic"::: "n" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: URYSOHN1:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 2) ($#k2_newton :::"|^"::: ) "n")) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k6_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k2_newton :::"|^"::: ) "n" ")" ))) ")" )) ")" )); end; :: deftheorem defines :::"dyadic"::: URYSOHN1:def 1 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 2) ($#k2_newton :::"|^"::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k6_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ))) ")" )) ")" )) ")" ))); definitionfunc :::"DYADIC"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: URYSOHN1:def 2 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n"))))) ")" )); end; :: deftheorem defines :::"DYADIC"::: URYSOHN1:def 2 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k2_urysohn1 :::"DYADIC"::: ) )) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n"))))) ")" )) ")" )); definitionfunc :::"DOM"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: URYSOHN1:def 3 (Set (Set "(" (Set "(" ($#k10_prob_1 :::"halfline"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k2_urysohn1 :::"DYADIC"::: ) ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Num 1) ")" )); end; :: deftheorem defines :::"DOM"::: URYSOHN1:def 3 : (Bool (Set ($#k3_urysohn1 :::"DOM"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k10_prob_1 :::"halfline"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k2_urysohn1 :::"DYADIC"::: ) ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Num 1) ")" ))); definitionlet "T" be ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "A")) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "T"))) ")" ); let "r" be ($#m2_subset_1 :::"Element"::: ) "of" (Set (Const "A")); :: original: :::"."::: redefine func "F" :::"."::: "r" -> ($#m1_subset_1 :::"Subset":::) "of" "T"; end; theorem :: URYSOHN1:1 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) ")" ))) ; theorem :: URYSOHN1:2 (Bool (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) )) ; theorem :: URYSOHN1:3 (Bool (Set ($#k1_urysohn1 :::"dyadic"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k8_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Num 1) ($#k8_domain_1 :::"}"::: ) )) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k1_urysohn1 :::"dyadic"::: ) "n") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"dyad"::: "n" -> ($#m1_hidden :::"FinSequence":::) means :: URYSOHN1:def 4 (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set "(" (Num 2) ($#k2_newton :::"|^"::: ) "n" ")" ) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "i")) ($#k5_real_1 :::"-"::: ) (Num 1) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k2_newton :::"|^"::: ) "n" ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"dyad"::: URYSOHN1:def 4 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_urysohn1 :::"dyad"::: ) (Set (Var "n")))) "iff" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set "(" (Num 2) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b2"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "i")) ($#k5_real_1 :::"-"::: ) (Num 1) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ))) ")" ) ")" ) ")" ))); theorem :: URYSOHN1:4 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k5_urysohn1 :::"dyad"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k5_urysohn1 :::"dyad"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n")))) ")" )) ; registration cluster (Set ($#k2_urysohn1 :::"DYADIC"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registration cluster (Set ($#k3_urysohn1 :::"DOM"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: URYSOHN1:5 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) ; theorem :: URYSOHN1:6 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n")))) & (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n")))) ")" )) ; theorem :: URYSOHN1:7 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 2) ($#k13_newton :::"|^"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "i")) ($#k4_nat_1 :::"*"::: ) (Num 2) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_urysohn1 :::"dyadic"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n")) ")" )))) ; theorem :: URYSOHN1:8 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Num 2) ($#k13_newton :::"|^"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "i")) ($#k4_nat_1 :::"*"::: ) (Num 2) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_urysohn1 :::"dyadic"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n")) ")" )))) ; theorem :: URYSOHN1:9 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_urysohn1 :::"dyadic"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n")) ")" )))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "x" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Const "n"))); func :::"axis"::: "x" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: URYSOHN1:def 5 (Bool "x" ($#r1_hidden :::"="::: ) (Set it ($#k6_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k2_newton :::"|^"::: ) "n" ")" ))); end; :: deftheorem defines :::"axis"::: URYSOHN1:def 5 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_urysohn1 :::"axis"::: ) (Set (Var "x")))) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b3")) ($#k6_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ))) ")" )))); theorem :: URYSOHN1:10 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_urysohn1 :::"axis"::: ) (Set (Var "x")) ")" ) ($#k6_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set (Var "n")) ")" ))) & (Bool (Set ($#k6_urysohn1 :::"axis"::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 2) ($#k13_newton :::"|^"::: ) (Set (Var "n")))) ")" ))) ; theorem :: URYSOHN1:11 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k6_urysohn1 :::"axis"::: ) (Set (Var "x")) ")" ) ($#k5_real_1 :::"-"::: ) (Num 1) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set (Var "n")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set "(" ($#k6_urysohn1 :::"axis"::: ) (Set (Var "x")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set (Var "n")) ")" ))) ")" ))) ; theorem :: URYSOHN1:12 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set "(" (Set "(" ($#k6_urysohn1 :::"axis"::: ) (Set (Var "x")) ")" ) ($#k5_real_1 :::"-"::: ) (Num 1) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set (Var "n")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set "(" ($#k6_urysohn1 :::"axis"::: ) (Set (Var "x")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set (Var "n")) ")" ))))) ; theorem :: URYSOHN1:13 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n")))))) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k6_urysohn1 :::"axis"::: ) (Set (Var "x")) ")" ) ($#k5_real_1 :::"-"::: ) (Num 1) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n")))) & (Bool (Set (Set "(" (Set "(" ($#k6_urysohn1 :::"axis"::: ) (Set (Var "x")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n")))) ")" ))) ; theorem :: URYSOHN1:14 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "x2")))) "holds" (Bool (Set ($#k6_urysohn1 :::"axis"::: ) (Set (Var "x1"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_urysohn1 :::"axis"::: ) (Set (Var "x2")))))) ; theorem :: URYSOHN1:15 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "x1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "x2")))) "holds" (Bool "(" (Bool (Set (Var "x1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k6_urysohn1 :::"axis"::: ) (Set (Var "x2")) ")" ) ($#k5_real_1 :::"-"::: ) (Num 1) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Set "(" (Set "(" ($#k6_urysohn1 :::"axis"::: ) (Set (Var "x1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set (Var "n")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x2"))) ")" ))) ; theorem :: URYSOHN1:16 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) "st" (Bool (Bool (Set (Var "x1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "x2"))) & (Bool (Bool "not" (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n"))))) & (Bool (Bool "not" (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n")))))) "holds" (Bool (Set (Set "(" (Set "(" ($#k6_urysohn1 :::"axis"::: ) (Set (Var "x1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k6_urysohn1 :::"axis"::: ) (Set (Var "x2")) ")" ) ($#k5_real_1 :::"-"::: ) (Num 1) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))))) ; begin notationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); synonym :::"Nbhd"::: "of" "x" "," "T" for :::"a_neighborhood"::: "of" "x"; end; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); redefine mode :::"a_neighborhood"::: "of" "x" means :: URYSOHN1:def 6 (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool "x" ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) it) ")" )); end; :: deftheorem defines :::"Nbhd"::: URYSOHN1:def 6 : (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 "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T")))) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_connsp_2 :::"Nbhd"::: ) "of" (Set (Var "x")) "," (Set (Var "T"))) "iff" (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "b3"))) ")" )) ")" )))); theorem :: URYSOHN1:17 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (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 "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "B")) "being" ($#m1_connsp_2 :::"Nbhd"::: ) "of" (Set (Var "x")) "," (Set (Var "T")) "st" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))))) ")" ))) ; theorem :: URYSOHN1:18 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "A")) "is" ($#m1_connsp_2 :::"Nbhd"::: ) "of" (Set (Var "x")) "," (Set (Var "T"))) ")" )) "holds" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ))) ; definitionlet "T" be ($#l1_pre_topc :::"TopSpace":::); redefine attr "T" is :::"T_1"::: means :: URYSOHN1:def 7 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" "T" "st" (Bool (Bool (Bool "not" (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q"))))) "holds" (Bool "ex" (Set (Var "W")) "," (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool "(" (Bool (Set (Var "W")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) & (Bool (Bool "not" (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Bool "not" (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "V")))) ")" ))); end; :: deftheorem defines :::"T_1"::: URYSOHN1:def 7 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v7_pre_topc :::"T_1"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Bool "not" (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q"))))) "holds" (Bool "ex" (Set (Var "W")) "," (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "W")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) & (Bool (Bool "not" (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Bool "not" (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "V")))) ")" ))) ")" )); theorem :: URYSOHN1:19 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v7_pre_topc :::"T_1"::: ) ) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ) "is" ($#v4_pre_topc :::"closed"::: ) )) ")" )) ; theorem :: URYSOHN1:20 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "T")) "is" ($#v10_pre_topc :::"normal"::: ) )) "holds" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool "ex" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "C")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) ")" )))) ; theorem :: URYSOHN1:21 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v9_pre_topc :::"regular"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (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 "B")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) ")" )))) ")" )) ; theorem :: URYSOHN1:22 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "T")) "is" ($#v10_pre_topc :::"normal"::: ) ) & (Bool (Set (Var "T")) "is" ($#v7_pre_topc :::"T_1"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) ")" )))) ; theorem :: URYSOHN1:23 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "T")) "is" ($#v10_pre_topc :::"normal"::: ) )) "holds" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "B")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "C")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) ")" )))) ; begin definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "A", "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); assume (Bool "(" (Bool (Set (Const "T")) "is" ($#v10_pre_topc :::"normal"::: ) ) & (Bool (Set (Const "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Const "A")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Const "B")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Const "A"))) ($#r1_tarski :::"c="::: ) (Set (Const "B"))) ")" ) ; mode :::"Between"::: "of" "A" "," "B" -> ($#m1_subset_1 :::"Subset":::) "of" "T" means :: URYSOHN1:def 8 (Bool "(" (Bool it ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool it "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) "A") ($#r1_tarski :::"c="::: ) it) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) it) ($#r1_tarski :::"c="::: ) "B") ")" ); end; :: deftheorem defines :::"Between"::: URYSOHN1:def 8 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v10_pre_topc :::"normal"::: ) ) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "B")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m1_urysohn1 :::"Between"::: ) "of" (Set (Var "A")) "," (Set (Var "B"))) "iff" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "b4")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Var "b4"))) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "b4"))) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) ")" ) ")" )))); theorem :: URYSOHN1:24 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "T")) "is" ($#v10_pre_topc :::"normal"::: ) )) "holds" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ))) & (Bool "(" "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r2")))) "holds" (Bool "(" (Bool (Set (Set (Var "G")) ($#k4_urysohn1 :::"."::: ) (Set (Var "r1"))) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Set (Var "G")) ($#k4_urysohn1 :::"."::: ) (Set (Var "r2"))) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "G")) ($#k4_urysohn1 :::"."::: ) (Set (Var "r1")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G")) ($#k4_urysohn1 :::"."::: ) (Set (Var "r2")))) ")" ) ")" )) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_urysohn1 :::"dyadic"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ")" ) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ))) & (Bool "(" "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) "st" (Bool (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r2")))) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k4_urysohn1 :::"."::: ) (Set (Var "r1"))) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Set (Var "F")) ($#k4_urysohn1 :::"."::: ) (Set (Var "r2"))) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "F")) ($#k4_urysohn1 :::"."::: ) (Set (Var "r1")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "F")) ($#k4_urysohn1 :::"."::: ) (Set (Var "r2")))) & "(" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n"))))) "implies" (Bool (Set (Set (Var "F")) ($#k4_urysohn1 :::"."::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "r")))) ")" ")" ) ")" ) ")" )))))) ;