:: FCONT_2  semantic presentation begin  

































definitionlet "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ); attr "f" is  :::"uniformly_continuous":::  means :: FCONT_2:def 1 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))) "holds"  (Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s"))) & (Bool  "("   "for" (Set (Var "x1")) "," (Set (Var "x2")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  "f")) & (Bool (Set (Var "x2"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  "f")) & (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "x1"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x2")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s")))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set  "(" "f"  ($#k1_seq_1 :::"."::: )  (Set (Var "x1")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" "f"  ($#k1_seq_1 :::"."::: )  (Set (Var "x2")) ")" ) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))  ")" )  ")" ))); end; 




:: deftheorem    defines :::"uniformly_continuous"::: FCONT_2:def 1 :  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v1_fcont_2 :::"uniformly_continuous"::: )  ) "iff" (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))) "holds"  (Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s"))) & (Bool  "("   "for" (Set (Var "x1")) "," (Set (Var "x2")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "x2"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "x1"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x2")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s")))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x1")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x2")) ")" ) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))  ")" )  ")" )))  ")" )); 
 
theorem :: FCONT_2:1 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_fcont_2 :::"uniformly_continuous"::: )  ) "iff" (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))) "holds"  (Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s"))) & (Bool  "("   "for" (Set (Var "x1")) "," (Set (Var "x2")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X")) ")" ))) & (Bool (Set (Var "x2"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X")) ")" ))) & (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "x1"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x2")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s")))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x1")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x2")) ")" ) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))  ")" )  ")" )))  ")" ))) ; 
 
theorem :: FCONT_2:2 (Bool  "for" (Set (Var "X")) "," (Set (Var "X1")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_fcont_2 :::"uniformly_continuous"::: )  ) & (Bool (Set (Var "X1"))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X1"))) "is"   ($#v1_fcont_2 :::"uniformly_continuous"::: )  ))) ; 
 
theorem :: FCONT_2:3 (Bool  "for" (Set (Var "X")) "," (Set (Var "X1")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f1")))) & (Bool (Set (Var "X1"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f2")))) & (Bool (Set (Set (Var "f1"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_fcont_2 :::"uniformly_continuous"::: )  ) & (Bool (Set (Set (Var "f2"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X1"))) "is"   ($#v1_fcont_2 :::"uniformly_continuous"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "X1")) ")" )) "is"   ($#v1_fcont_2 :::"uniformly_continuous"::: )  ))) ; 
 
theorem :: FCONT_2:4 (Bool  "for" (Set (Var "X")) "," (Set (Var "X1")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f1")))) & (Bool (Set (Var "X1"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f2")))) & (Bool (Set (Set (Var "f1"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_fcont_2 :::"uniformly_continuous"::: )  ) & (Bool (Set (Set (Var "f2"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X1"))) "is"   ($#v1_fcont_2 :::"uniformly_continuous"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "f2")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "X1")) ")" )) "is"   ($#v1_fcont_2 :::"uniformly_continuous"::: )  ))) ; 
 
theorem :: FCONT_2:5 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_fcont_2 :::"uniformly_continuous"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_fcont_2 :::"uniformly_continuous"::: )  )))) ; 
 
theorem :: FCONT_2:6 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_fcont_2 :::"uniformly_continuous"::: )  )) "holds"  (Bool (Set (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set (Var "f")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_fcont_2 :::"uniformly_continuous"::: )  ))) ; 
 
theorem :: FCONT_2:7 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_fcont_2 :::"uniformly_continuous"::: )  )) "holds"  (Bool (Set (Set  "("  ($#k56_valued_1 :::"abs"::: )  (Set (Var "f")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_fcont_2 :::"uniformly_continuous"::: )  ))) ; 
 
theorem :: FCONT_2:8 (Bool  "for" (Set (Var "X")) "," (Set (Var "X1")) "," (Set (Var "Z")) "," (Set (Var "Z1")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f1")))) & (Bool (Set (Var "X1"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f2")))) & (Bool (Set (Set (Var "f1"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_fcont_2 :::"uniformly_continuous"::: )  ) & (Bool (Set (Set (Var "f2"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X1"))) "is"   ($#v1_fcont_2 :::"uniformly_continuous"::: )  ) & (Bool (Set (Set (Var "f1"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "Z"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) & (Bool (Set (Set (Var "f2"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "Z1"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z")) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "X1")) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z1")) ")" )) "is"   ($#v1_fcont_2 :::"uniformly_continuous"::: )  ))) ; 
 
theorem :: FCONT_2:9 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_fcont_2 :::"uniformly_continuous"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  ))) ; 
 
theorem :: FCONT_2:10 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v2_fcont_1 :::"Lipschitzian"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_fcont_2 :::"uniformly_continuous"::: )  ))) ; 
 
theorem :: FCONT_2:11 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "Y")) "is"   ($#v1_rcomp_1 :::"compact"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v1_fcont_2 :::"uniformly_continuous"::: )  ))) ; 
 
theorem :: FCONT_2:12 (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "Y")) "is"   ($#v1_rcomp_1 :::"compact"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v1_fcont_2 :::"uniformly_continuous"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "Y"))) "is"   ($#v1_rcomp_1 :::"compact"::: )  ))) ; 
 
theorem :: FCONT_2:13 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "Y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "Y")) "is"   ($#v1_rcomp_1 :::"compact"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v1_fcont_2 :::"uniformly_continuous"::: )  )) "holds"  (Bool  "ex" (Set (Var "x1")) "," (Set (Var "x2")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "x1"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))) & (Bool (Set (Var "x2"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x1")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "Y")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x2")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "Y")) ")" )))  ")" )))) ; 
 
theorem :: FCONT_2:14 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is" bbbadV3_FUNCT_1())) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_fcont_2 :::"uniformly_continuous"::: )  ))) ; 
 
theorem :: FCONT_2:15 (Bool  "for" (Set (Var "p")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "g"))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )) "is"   ($#v1_fcont_1 :::"continuous"::: )  )) "holds"  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "p")) ")" ) "," (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "g")) ")" ) ($#k1_rcomp_1 :::".]"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "g")) ")" ) "," (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "p")) ")" ) ($#k1_rcomp_1 :::".]"::: ) )))) "holds"  (Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "s"))))  ")" ))))) ; 
 
theorem :: FCONT_2:16 (Bool  "for" (Set (Var "p")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "g"))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )) "is"   ($#v1_fcont_1 :::"continuous"::: )  )) "holds"  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ")" ) "," (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "s"))))  ")" ))))) ; 
 
theorem :: FCONT_2:17 (Bool  "for" (Set (Var "p")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "g"))) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool (Bool  "not" (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )) "is"   ($#v5_valued_0 :::"increasing"::: )  ))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )) "is"   ($#v6_valued_0 :::"decreasing"::: )  ))) ; 
 
theorem :: FCONT_2:18 (Bool  "for" (Set (Var "p")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "g"))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool  "not" (Bool  "("  (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "p")))) & (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "g"))))  ")" ))) "holds"  (Bool  "("  (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "g")))) & (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "p"))))  ")" ))) ; 
 
theorem :: FCONT_2:19 (Bool  "for" (Set (Var "p")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "g"))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )) "is"   ($#v1_fcont_1 :::"continuous"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ")" ) "," (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ")" ) ($#k1_rcomp_1 :::".]"::: ) )))) ; 
 
theorem :: FCONT_2:20 (Bool  "for" (Set (Var "p")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v2_funct_1 :::"one-to-one"::: )    ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "g"))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )) "is"   ($#v1_fcont_1 :::"continuous"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k2_partfun2 :::"""::: )  ")" )  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ")" ) "," (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) "is"   ($#v1_fcont_1 :::"continuous"::: )  ))) ;