:: URYSOHN3 semantic presentation begin theorem :: URYSOHN3:1 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_pre_topc :::"normal"::: ) ($#l1_pre_topc :::"TopSpace":::) (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 :::"{}"::: ) )) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k9_setfam_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")))) ")" ) ")" ) ")" ))))) ; 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")); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); 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" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Const "B")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Const "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Const "B"))) ")" ) ; mode :::"Drizzle"::: "of" "A" "," "B" "," "n" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_urysohn1 :::"dyadic"::: ) "n" ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ")" ) means :: URYSOHN3:def 1 (Bool "(" (Bool "A" ($#r1_tarski :::"c="::: ) (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "B" ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_struct_0 :::"[#]"::: ) "T" ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" it ($#k1_funct_1 :::"."::: ) (Num 1) ")" ))) & (Bool "(" "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k1_urysohn1 :::"dyadic"::: ) "n") "st" (Bool (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r2")))) "holds" (Bool "(" (Bool (Set it ($#k4_urysohn1 :::"."::: ) (Set (Var "r1"))) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set it ($#k4_urysohn1 :::"."::: ) (Set (Var "r2"))) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" it ($#k4_urysohn1 :::"."::: ) (Set (Var "r1")) ")" )) ($#r1_tarski :::"c="::: ) (Set it ($#k4_urysohn1 :::"."::: ) (Set (Var "r2")))) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"Drizzle"::: URYSOHN3:def 1 : (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")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "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" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "B")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) "is" ($#m1_urysohn3 :::"Drizzle"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "n"))) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "b5")) ($#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 "b5")) ($#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 "b5")) ($#k4_urysohn1 :::"."::: ) (Set (Var "r1"))) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Set (Var "b5")) ($#k4_urysohn1 :::"."::: ) (Set (Var "r2"))) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "b5")) ($#k4_urysohn1 :::"."::: ) (Set (Var "r1")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "b5")) ($#k4_urysohn1 :::"."::: ) (Set (Var "r2")))) ")" ) ")" ) ")" ) ")" ))))); theorem :: URYSOHN3:2 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_pre_topc :::"normal"::: ) ($#l1_pre_topc :::"TopSpace":::) (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 :::"{}"::: ) )) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_urysohn3 :::"Drizzle"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "n")) (Bool "ex" (Set (Var "F")) "being" ($#m1_urysohn3 :::"Drizzle"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)) "st" (Bool "for" (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 "r")) ($#r2_hidden :::"in"::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "F")) ($#k4_urysohn1 :::"."::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "r")))))))))) ; theorem :: URYSOHN3:3 (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")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_urysohn3 :::"Drizzle"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "n")) "holds" (Bool (Set (Var "S")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set ($#k2_urysohn1 :::"DYADIC"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ")" ) ")" )))))) ; definitionlet "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Const "A")) "," (Set (Const "B")) ")" ")" ); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); :: original: :::"."::: redefine func "F" :::"."::: "n" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" "A" "," "B" ")" ); end; theorem :: URYSOHN3:4 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_pre_topc :::"normal"::: ) ($#l1_pre_topc :::"TopSpace":::) (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 :::"{}"::: ) )) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set ($#k2_urysohn1 :::"DYADIC"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ")" ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k1_urysohn3 :::"."::: ) (Set (Var "n"))) "is" ($#m1_urysohn3 :::"Drizzle"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "n"))) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k1_urysohn3 :::"."::: ) (Set (Var "n")) ")" )) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k1_urysohn3 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k1_urysohn3 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "r")))) ")" ) ")" ))))) ; 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" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Const "B")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Const "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Const "B"))) ")" ) ; mode :::"Rain"::: "of" "A" "," "B" -> ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set ($#k2_urysohn1 :::"DYADIC"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ")" ) means :: URYSOHN3:def 2 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set it ($#k1_urysohn3 :::"."::: ) (Set (Var "n"))) "is" ($#m1_urysohn3 :::"Drizzle"::: ) "of" "A" "," "B" "," (Set (Var "n"))) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" it ($#k1_urysohn3 :::"."::: ) (Set (Var "n")) ")" )) "holds" (Bool (Set (Set "(" it ($#k1_urysohn3 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set "(" it ($#k1_urysohn3 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "r")))) ")" ) ")" )); end; :: deftheorem defines :::"Rain"::: URYSOHN3:def 2 : (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" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "B")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set ($#k2_urysohn1 :::"DYADIC"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m2_urysohn3 :::"Rain"::: ) "of" (Set (Var "A")) "," (Set (Var "B"))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "b4")) ($#k1_urysohn3 :::"."::: ) (Set (Var "n"))) "is" ($#m1_urysohn3 :::"Drizzle"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "n"))) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "b4")) ($#k1_urysohn3 :::"."::: ) (Set (Var "n")) ")" )) "holds" (Bool (Set (Set "(" (Set (Var "b4")) ($#k1_urysohn3 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b4")) ($#k1_urysohn3 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "r")))) ")" ) ")" )) ")" )))); definitionlet "x" be ($#m1_subset_1 :::"Real":::); assume (Bool (Set (Const "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_urysohn1 :::"DYADIC"::: ) )) ; func :::"inf_number_dyadic"::: "x" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: URYSOHN3:def 3 (Bool "(" "(" (Bool (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "implies" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Bool "not" "x" ($#r2_hidden :::"in"::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n")))))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1))) ")" ) ")" ); end; :: deftheorem defines :::"inf_number_dyadic"::: URYSOHN3:def 3 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_urysohn1 :::"DYADIC"::: ) ))) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_urysohn3 :::"inf_number_dyadic"::: ) (Set (Var "x")))) "iff" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "implies" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n")))))) "holds" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1))) ")" ) ")" ) ")" ))); theorem :: URYSOHN3:5 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_urysohn1 :::"DYADIC"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set "(" ($#k2_urysohn3 :::"inf_number_dyadic"::: ) (Set (Var "x")) ")" )))) ; theorem :: URYSOHN3:6 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_urysohn1 :::"DYADIC"::: ) ))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k2_urysohn3 :::"inf_number_dyadic"::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n")))))) ; theorem :: URYSOHN3:7 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n"))))) "holds" (Bool (Set ($#k2_urysohn3 :::"inf_number_dyadic"::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))))) ; theorem :: URYSOHN3:8 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_pre_topc :::"normal"::: ) ($#l1_pre_topc :::"TopSpace":::) (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 :::"{}"::: ) )) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "G")) "being" ($#m2_urysohn3 :::"Rain"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_urysohn1 :::"DYADIC"::: ) ))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k1_urysohn3 :::"."::: ) (Set "(" ($#k2_urysohn3 :::"inf_number_dyadic"::: ) (Set (Var "x")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k1_urysohn3 :::"."::: ) (Set "(" (Set "(" ($#k2_urysohn3 :::"inf_number_dyadic"::: ) (Set (Var "x")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))))))) ; theorem :: URYSOHN3:9 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_pre_topc :::"normal"::: ) ($#l1_pre_topc :::"TopSpace":::) (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 :::"{}"::: ) )) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "G")) "being" ($#m2_urysohn3 :::"Rain"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_urysohn1 :::"DYADIC"::: ) ))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k1_urysohn3 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))))))))) ; theorem :: URYSOHN3:10 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_pre_topc :::"normal"::: ) ($#l1_pre_topc :::"TopSpace":::) (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 :::"{}"::: ) )) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "G")) "being" ($#m2_urysohn3 :::"Rain"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k3_urysohn1 :::"DOM"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ")" ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_urysohn1 :::"DOM"::: ) ))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_prob_1 :::"halfline"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "implies" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Num 1)))) "implies" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T")))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_urysohn1 :::"DYADIC"::: ) ))) "implies" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k1_urysohn3 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) ")" ")" )))))) ; 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" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Const "B")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Const "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Const "B"))) ")" ) ; let "R" be ($#m2_urysohn3 :::"Rain"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); func :::"Tempest"::: "R" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k3_urysohn1 :::"DOM"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ")" ) means :: URYSOHN3:def 4 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_urysohn1 :::"DOM"::: ) ))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_prob_1 :::"halfline"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Num 1)))) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_urysohn1 :::"DYADIC"::: ) ))) "implies" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n"))))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "R" ($#k1_urysohn3 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) ")" ")" )); end; :: deftheorem defines :::"Tempest"::: URYSOHN3:def 4 : (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" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "B")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "R")) "being" ($#m2_urysohn3 :::"Rain"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k3_urysohn1 :::"DOM"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k3_urysohn3 :::"Tempest"::: ) (Set (Var "R")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_urysohn1 :::"DOM"::: ) ))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_prob_1 :::"halfline"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "implies" (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Num 1)))) "implies" (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T")))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_urysohn1 :::"DYADIC"::: ) ))) "implies" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_urysohn1 :::"dyadic"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R")) ($#k1_urysohn3 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) ")" ")" )) ")" ))))); definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "T" be ($#l1_pre_topc :::"TopSpace":::); let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "T"))) ")" ); let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); :: original: :::"."::: redefine func "F" :::"."::: "x" -> ($#m1_subset_1 :::"Subset":::) "of" "T"; end; theorem :: URYSOHN3:11 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_pre_topc :::"normal"::: ) ($#l1_pre_topc :::"TopSpace":::) (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 :::"{}"::: ) )) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "G")) "being" ($#m2_urysohn3 :::"Rain"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_urysohn3 :::"Tempest"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "r")))) & (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k3_urysohn1 :::"DOM"::: ) ))) "holds" (Bool (Set (Var "C")) "is" ($#v3_pre_topc :::"open"::: ) )))))) ; theorem :: URYSOHN3:12 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_pre_topc :::"normal"::: ) ($#l1_pre_topc :::"TopSpace":::) (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 :::"{}"::: ) )) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "G")) "being" ($#m2_urysohn3 :::"Rain"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) (Set ($#k3_urysohn1 :::"DOM"::: ) )) & (Bool (Set (Var "r2")) ($#r2_hidden :::"in"::: ) (Set ($#k3_urysohn1 :::"DOM"::: ) )) & (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r2")))) "holds" (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_urysohn3 :::"Tempest"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "r1"))))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k3_urysohn3 :::"Tempest"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "r2"))))))))) ; 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")); let "G" be ($#m2_urysohn3 :::"Rain"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); let "p" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); func :::"Rainbow"::: "(" "p" "," "G" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: URYSOHN3:def 5 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_urysohn1 :::"DYADIC"::: ) )) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Var "x")))) "holds" (Bool "not" (Bool "p" ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k3_urysohn3 :::"Tempest"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))))) ")" ) ")" ) ")" )); end; :: deftheorem defines :::"Rainbow"::: URYSOHN3:def 5 : (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")) (Bool "for" (Set (Var "G")) "being" ($#m2_urysohn3 :::"Rain"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set ($#k5_urysohn3 :::"Rainbow"::: ) "(" (Set (Var "p")) "," (Set (Var "G")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b6"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_urysohn1 :::"DYADIC"::: ) )) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Var "x")))) "holds" (Bool "not" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k3_urysohn3 :::"Tempest"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))))) ")" ) ")" ) ")" )) ")" )))))); theorem :: URYSOHN3:13 (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")) (Bool "for" (Set (Var "G")) "being" ($#m2_urysohn3 :::"Rain"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k5_urysohn3 :::"Rainbow"::: ) "(" (Set (Var "p")) "," (Set (Var "G")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_urysohn1 :::"DYADIC"::: ) )))))) ; 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")); let "R" be ($#m2_urysohn3 :::"Rain"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); func :::"Thunder"::: "R" -> ($#m1_subset_1 :::"Function":::) "of" "T" "," (Set ($#k3_topmetr :::"R^1"::: ) ) means :: URYSOHN3:def 6 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" "T" "holds" (Bool "(" "(" (Bool (Bool (Set ($#k5_urysohn3 :::"Rainbow"::: ) "(" (Set (Var "p")) "," "R" ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & (Bool "(" "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k5_urysohn3 :::"Rainbow"::: ) "(" (Set (Var "p")) "," "R" ")" ))) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k8_supinf_2 :::"sup"::: ) (Set (Var "S")))) ")" ) ")" )); end; :: deftheorem defines :::"Thunder"::: URYSOHN3:def 6 : (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")) (Bool "for" (Set (Var "R")) "being" ($#m2_urysohn3 :::"Rain"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k6_urysohn3 :::"Thunder"::: ) (Set (Var "R")))) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k5_urysohn3 :::"Rainbow"::: ) "(" (Set (Var "p")) "," (Set (Var "R")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Set (Var "b5")) ($#k1_seq_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & (Bool "(" "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k5_urysohn3 :::"Rainbow"::: ) "(" (Set (Var "p")) "," (Set (Var "R")) ")" ))) "holds" (Bool (Set (Set (Var "b5")) ($#k1_seq_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k8_supinf_2 :::"sup"::: ) (Set (Var "S")))) ")" ) ")" )) ")" ))))); theorem :: URYSOHN3:14 (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")) (Bool "for" (Set (Var "G")) "being" ($#m2_urysohn3 :::"Rain"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k5_urysohn3 :::"Rainbow"::: ) "(" (Set (Var "p")) "," (Set (Var "G")) ")" ))) "holds" (Bool "for" (Set (Var "e1")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool (Set (Var "e1")) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "(" (Bool (Set ($#k1_supinf_2 :::"0."::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k8_supinf_2 :::"sup"::: ) (Set (Var "S")))) & (Bool (Set ($#k8_supinf_2 :::"sup"::: ) (Set (Var "S"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "e1"))) ")" ))))))) ; theorem :: URYSOHN3:15 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_pre_topc :::"normal"::: ) ($#l1_pre_topc :::"TopSpace":::) (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 :::"{}"::: ) )) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "G")) "being" ($#m2_urysohn3 :::"Rain"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "r")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_urysohn1 :::"DOM"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Set "(" ($#k6_urysohn3 :::"Thunder"::: ) (Set (Var "G")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k3_urysohn3 :::"Tempest"::: ) (Set (Var "G")) ")" ) ($#k4_urysohn3 :::"."::: ) (Set (Var "r"))))))))) ; theorem :: URYSOHN3:16 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_pre_topc :::"normal"::: ) ($#l1_pre_topc :::"TopSpace":::) (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 :::"{}"::: ) )) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "G")) "being" ($#m2_urysohn3 :::"Rain"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Set ($#k2_urysohn1 :::"DYADIC"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Num 1) ")" ))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "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 (Set "(" ($#k3_urysohn3 :::"Tempest"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "r"))))) "holds" (Bool (Set (Set "(" ($#k6_urysohn3 :::"Thunder"::: ) (Set (Var "G")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r")))))))) ; theorem :: URYSOHN3:17 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_pre_topc :::"normal"::: ) ($#l1_pre_topc :::"TopSpace":::) (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 :::"{}"::: ) )) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "G")) "being" ($#m2_urysohn3 :::"Rain"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "r1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_urysohn1 :::"DOM"::: ) ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r1")))) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k6_urysohn3 :::"Thunder"::: ) (Set (Var "G")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "p"))))) "holds" (Bool "not" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k3_urysohn3 :::"Tempest"::: ) (Set (Var "G")) ")" ) ($#k4_urysohn3 :::"."::: ) (Set (Var "r1")))))))))) ; theorem :: URYSOHN3:18 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_pre_topc :::"normal"::: ) ($#l1_pre_topc :::"TopSpace":::) (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 :::"{}"::: ) )) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "G")) "being" ($#m2_urysohn3 :::"Rain"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set ($#k6_urysohn3 :::"Thunder"::: ) (Set (Var "G"))) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k6_urysohn3 :::"Thunder"::: ) (Set (Var "G")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set "(" ($#k6_urysohn3 :::"Thunder"::: ) (Set (Var "G")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "implies" (Bool (Set (Set "(" ($#k6_urysohn3 :::"Thunder"::: ) (Set (Var "G")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "implies" (Bool (Set (Set "(" ($#k6_urysohn3 :::"Thunder"::: ) (Set (Var "G")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ")" ) ")" ) ")" )))) ; theorem :: URYSOHN3:19 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_pre_topc :::"normal"::: ) ($#l1_pre_topc :::"TopSpace":::) (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 :::"{}"::: ) )) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "implies" (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "implies" (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ")" ) ")" ) ")" )))) ; theorem :: URYSOHN3:20 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v10_pre_topc :::"normal"::: ) ($#l1_pre_topc :::"TopSpace":::) (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_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "implies" (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "implies" (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ")" ) ")" ) ")" )))) ; theorem :: URYSOHN3:21 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_pre_topc :::"T_2"::: ) ($#v1_compts_1 :::"compact"::: ) ($#l1_pre_topc :::"TopSpace":::) (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_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "implies" (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "implies" (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ")" ) ")" ) ")" )))) ;