:: URYSOHN2  semantic presentation begin  
theorem :: URYSOHN2:1 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k2_real_1 :::"""::: )  ")" )  ($#k1_integra2 :::"**"::: )  (Set  "(" (Set (Var "x"))  ($#k1_integra2 :::"**"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "A"))))) ; 
 
theorem :: URYSOHN2:2 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_integra2 :::"**"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "A"))))) ; 
 
theorem :: URYSOHN2:3 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k1_integra2 :::"**"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_seq_4 :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_seq_4 :::"}"::: ) ))) ; 
 
theorem :: URYSOHN2:4 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_integra2 :::"**"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: URYSOHN2:5 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"R_eal":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) "or" (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_supinf_1 :::"-infty"::: )  )) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_supinf_1 :::"-infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_supinf_1 :::"-infty"::: )  )) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_supinf_1 :::"-infty"::: )  )) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_1 :::"+infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  )) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  )) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_1 :::"+infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_1 :::"+infty"::: )  )) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_1 :::"+infty"::: )  ))  ")" )  ")" )) ; 
 
theorem :: URYSOHN2:6 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Interval":::) "holds"  (Bool (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k1_integra2 :::"**"::: )  (Set (Var "A"))) "is"   ($#v6_xxreal_2 :::"interval"::: )  )) ; 
 
theorem :: URYSOHN2:7 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Interval":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "A")) "is"   ($#v1_measure5 :::"open_interval"::: )  )) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_integra2 :::"**"::: )  (Set (Var "A"))) "is"   ($#v1_measure5 :::"open_interval"::: )  ))) ; 
 
theorem :: URYSOHN2:8 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Interval":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "A")) "is"   ($#v2_measure5 :::"closed_interval"::: )  )) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_integra2 :::"**"::: )  (Set (Var "A"))) "is"   ($#v2_measure5 :::"closed_interval"::: )  ))) ; 
 
theorem :: URYSOHN2:9 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Interval":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x"))) & (Bool (Set (Var "A")) "is"   ($#v3_measure5 :::"right_open_interval"::: )  )) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_integra2 :::"**"::: )  (Set (Var "A"))) "is"   ($#v3_measure5 :::"right_open_interval"::: )  ))) ; 
 
theorem :: URYSOHN2:10 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Interval":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "A")) "is"   ($#v3_measure5 :::"right_open_interval"::: )  )) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_integra2 :::"**"::: )  (Set (Var "A"))) "is"   ($#v4_measure5 :::"left_open_interval"::: )  ))) ; 
 
theorem :: URYSOHN2:11 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Interval":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x"))) & (Bool (Set (Var "A")) "is"   ($#v4_measure5 :::"left_open_interval"::: )  )) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_integra2 :::"**"::: )  (Set (Var "A"))) "is"   ($#v4_measure5 :::"left_open_interval"::: )  ))) ; 
 
theorem :: URYSOHN2:12 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Interval":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "A")) "is"   ($#v4_measure5 :::"left_open_interval"::: )  )) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_integra2 :::"**"::: )  (Set (Var "A"))) "is"   ($#v3_measure5 :::"right_open_interval"::: )  ))) ; 
 
theorem :: URYSOHN2:13 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Interval":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x")))) "holds"  (Bool  "for" (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Interval":::)  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_integra2 :::"**"::: )  (Set (Var "A")))) & (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_xxreal_1 :::"[."::: ) (Set  "("  ($#k7_supinf_2 :::"inf"::: )  (Set (Var "A")) ")" ) "," (Set  "("  ($#k8_supinf_2 :::"sup"::: )  (Set (Var "A")) ")" ) ($#k1_xxreal_1 :::".]"::: ) ))) "holds"  (Bool  "("  (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_xxreal_1 :::"[."::: ) (Set  "("  ($#k7_supinf_2 :::"inf"::: )  (Set (Var "B")) ")" ) "," (Set  "("  ($#k8_supinf_2 :::"sup"::: )  (Set (Var "B")) ")" ) ($#k1_xxreal_1 :::".]"::: ) )) & (Bool  "("   "for" (Set (Var "s")) "," (Set (Var "t")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_supinf_2 :::"inf"::: )  (Set (Var "A")))) & (Bool (Set (Var "t"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_supinf_2 :::"sup"::: )  (Set (Var "A"))))) "holds"  (Bool  "("  (Bool (Set   ($#k7_supinf_2 :::"inf"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set (Var "s")))) & (Bool (Set   ($#k8_supinf_2 :::"sup"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set (Var "t"))))  ")" )  ")" )  ")" )))) ; 
 
theorem :: URYSOHN2:14 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Interval":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x")))) "holds"  (Bool  "for" (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Interval":::)  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_integra2 :::"**"::: )  (Set (Var "A")))) & (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k3_xxreal_1 :::"]."::: ) (Set  "("  ($#k7_supinf_2 :::"inf"::: )  (Set (Var "A")) ")" ) "," (Set  "("  ($#k8_supinf_2 :::"sup"::: )  (Set (Var "A")) ")" ) ($#k3_xxreal_1 :::".]"::: ) ))) "holds"  (Bool  "("  (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set  ($#k3_xxreal_1 :::"]."::: ) (Set  "("  ($#k7_supinf_2 :::"inf"::: )  (Set (Var "B")) ")" ) "," (Set  "("  ($#k8_supinf_2 :::"sup"::: )  (Set (Var "B")) ")" ) ($#k3_xxreal_1 :::".]"::: ) )) & (Bool  "("   "for" (Set (Var "s")) "," (Set (Var "t")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_supinf_2 :::"inf"::: )  (Set (Var "A")))) & (Bool (Set (Var "t"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_supinf_2 :::"sup"::: )  (Set (Var "A"))))) "holds"  (Bool  "("  (Bool (Set   ($#k7_supinf_2 :::"inf"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set (Var "s")))) & (Bool (Set   ($#k8_supinf_2 :::"sup"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set (Var "t"))))  ")" )  ")" )  ")" )))) ; 
 
theorem :: URYSOHN2:15 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Interval":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x")))) "holds"  (Bool  "for" (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Interval":::)  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_integra2 :::"**"::: )  (Set (Var "A")))) & (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_measure5 :::"]."::: ) (Set  "("  ($#k7_supinf_2 :::"inf"::: )  (Set (Var "A")) ")" ) "," (Set  "("  ($#k8_supinf_2 :::"sup"::: )  (Set (Var "A")) ")" ) ($#k1_measure5 :::".["::: ) ))) "holds"  (Bool  "("  (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_measure5 :::"]."::: ) (Set  "("  ($#k7_supinf_2 :::"inf"::: )  (Set (Var "B")) ")" ) "," (Set  "("  ($#k8_supinf_2 :::"sup"::: )  (Set (Var "B")) ")" ) ($#k1_measure5 :::".["::: ) )) & (Bool  "("   "for" (Set (Var "s")) "," (Set (Var "t")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_supinf_2 :::"inf"::: )  (Set (Var "A")))) & (Bool (Set (Var "t"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_supinf_2 :::"sup"::: )  (Set (Var "A"))))) "holds"  (Bool  "("  (Bool (Set   ($#k7_supinf_2 :::"inf"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set (Var "s")))) & (Bool (Set   ($#k8_supinf_2 :::"sup"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set (Var "t"))))  ")" )  ")" )  ")" )))) ; 
 
theorem :: URYSOHN2:16 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Interval":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x")))) "holds"  (Bool  "for" (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Interval":::)  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_integra2 :::"**"::: )  (Set (Var "A")))) & (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k2_xxreal_1 :::"[."::: ) (Set  "("  ($#k7_supinf_2 :::"inf"::: )  (Set (Var "A")) ")" ) "," (Set  "("  ($#k8_supinf_2 :::"sup"::: )  (Set (Var "A")) ")" ) ($#k2_xxreal_1 :::".["::: ) ))) "holds"  (Bool  "("  (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set  ($#k2_xxreal_1 :::"[."::: ) (Set  "("  ($#k7_supinf_2 :::"inf"::: )  (Set (Var "B")) ")" ) "," (Set  "("  ($#k8_supinf_2 :::"sup"::: )  (Set (Var "B")) ")" ) ($#k2_xxreal_1 :::".["::: ) )) & (Bool  "("   "for" (Set (Var "s")) "," (Set (Var "t")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_supinf_2 :::"inf"::: )  (Set (Var "A")))) & (Bool (Set (Var "t"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_supinf_2 :::"sup"::: )  (Set (Var "A"))))) "holds"  (Bool  "("  (Bool (Set   ($#k7_supinf_2 :::"inf"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set (Var "s")))) & (Bool (Set   ($#k8_supinf_2 :::"sup"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set (Var "t"))))  ")" )  ")" )  ")" )))) ; 
 
theorem :: URYSOHN2:17 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Interval":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_integra2 :::"**"::: )  (Set (Var "A"))) "is"   ($#m1_subset_1 :::"Interval":::)))) ; 
 registrationlet "A" be   ($#v6_xxreal_2 :::"interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ); let "x" be   ($#m1_subset_1 :::"Real":::); 
cluster (Set "x"  ($#k23_member_1 :::"**"::: )  "A") ->   ($#v6_xxreal_2 :::"interval"::: )   ; 
end; 
theorem :: URYSOHN2:18 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"R_eal":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y")))) "holds"  (Bool (Set   ($#k8_supinf_2 :::"sup"::: )  (Set  "(" (Set (Var "x"))  ($#k1_integra2 :::"**"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k1_extreal1 :::"*"::: )  (Set  "("  ($#k8_supinf_2 :::"sup"::: )  (Set (Var "A")) ")" )))))) ; 
 
theorem :: URYSOHN2:19 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"R_eal":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y")))) "holds"  (Bool (Set   ($#k7_supinf_2 :::"inf"::: )  (Set  "(" (Set (Var "x"))  ($#k1_integra2 :::"**"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k1_extreal1 :::"*"::: )  (Set  "("  ($#k7_supinf_2 :::"inf"::: )  (Set (Var "A")) ")" )))))) ; 
 
theorem :: URYSOHN2:20 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Interval":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x")))) "holds"  (Bool  "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_measure5 :::"diameter"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set (Var "x"))  ($#k8_real_1 :::"*"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_measure5 :::"diameter"::: )  (Set  "(" (Set (Var "x"))  ($#k1_integra2 :::"**"::: )  (Set (Var "A")) ")" )))))) ; 
 
theorem :: URYSOHN2:21 (Bool  "for" (Set (Var "eps")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "eps")))) "holds"  (Bool  "ex" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Num 2)  ($#k13_newton :::"|^"::: )  (Set (Var "n")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "eps")))))) ; 
 
theorem :: URYSOHN2:22 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "b"))  ($#k9_real_1 :::"-"::: )  (Set (Var "a"))))) "holds"  (Bool  "ex" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b")))  ")" ))) ; 
 
theorem :: URYSOHN2:23 (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   ($#k2_urysohn1 :::"DYADIC"::: )  ))) ; 
 
theorem :: URYSOHN2:24 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1))) "holds"  (Bool  "ex" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_urysohn1 :::"DYADIC"::: )  )) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "c"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b")))  ")" ))) ; 
 
theorem :: URYSOHN2:25 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b")))) "holds"  (Bool  "ex" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_urysohn1 :::"DOM"::: )  )) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "c"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b")))  ")" ))) ; 
 
theorem :: URYSOHN2:26 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k7_numbers :::"ExtREAL"::: ) )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"R_eal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set  ($#k1_xxreal_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_xxreal_1 :::".]"::: ) ))) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k7_supinf_2 :::"inf"::: )  (Set (Var "A")))) & (Bool (Set   ($#k8_supinf_2 :::"sup"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))  ")" ))) ; 
 
theorem :: URYSOHN2:27 (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_urysohn1 :::"DYADIC"::: )  )) & (Bool (Num 1)  ($#r2_hidden :::"in"::: )  (Set   ($#k2_urysohn1 :::"DYADIC"::: )  ))  ")" ) ; 
 
theorem :: URYSOHN2:28 (Bool (Set   ($#k2_urysohn1 :::"DYADIC"::: )  )  ($#r1_tarski :::"c="::: )  (Set  ($#k1_xxreal_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_xxreal_1 :::".]"::: ) )) ; 
 
theorem :: URYSOHN2:29 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))) "holds"  (Bool (Set   ($#k1_urysohn1 :::"dyadic"::: )  (Set (Var "n")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_urysohn1 :::"dyadic"::: )  (Set (Var "k"))))) ; 
 
theorem :: URYSOHN2:30 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "c"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "d"))) & (Bool (Set (Var "d"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b")))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "d"))  ($#k9_real_1 :::"-"::: )  (Set (Var "c")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "b"))  ($#k9_real_1 :::"-"::: )  (Set (Var "a"))))) ; 
 
theorem :: URYSOHN2:31 (Bool  "for" (Set (Var "eps")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "eps")))) "holds"  (Bool  "for" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "d")))) "holds"  (Bool  "ex" (Set (Var "r1")) "," (Set (Var "r2")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "r1"))  ($#r2_hidden :::"in"::: )  (Set (Set  ($#k2_urysohn1 :::"DYADIC"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k3_limfunc1 :::"right_open_halfline"::: )  (Num 1) ")" ))) & (Bool (Set (Var "r2"))  ($#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 "r1"))) & (Bool (Set (Var "r1"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "d"))) & (Bool (Set (Var "d"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r2"))) & (Bool (Set (Set (Var "r2"))  ($#k9_real_1 :::"-"::: )  (Set (Var "r1")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "eps")))  ")" )))) ; 
 begin  
theorem :: URYSOHN2:32 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k1_integra2 :::"**"::: )  (Set (Var "A"))) "is"   ($#v4_xxreal_2 :::"bounded_above"::: )  )) "holds"  (Bool (Set (Var "A")) "is"   ($#v4_xxreal_2 :::"bounded_above"::: )  ))) ; 
 
theorem :: URYSOHN2:33 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k1_integra2 :::"**"::: )  (Set (Var "A"))) "is"   ($#v3_xxreal_2 :::"bounded_below"::: )  )) "holds"  (Bool (Set (Var "A")) "is"   ($#v3_xxreal_2 :::"bounded_below"::: )  ))) ;