:: FCONT_3  semantic presentation begin  




























registration
cluster (Set   ($#k2_subset_1 :::"[#]"::: )  (Set  ($#k1_numbers :::"REAL"::: ) )) ->   ($#v2_rcomp_1 :::"closed"::: )   ; 

cluster   ($#v1_xboole_0 :::"empty"::: )    ->   ($#v2_rcomp_1 :::"closed"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  ($#k1_numbers :::"REAL"::: ) ))); 
end; registration
cluster (Set   ($#k2_subset_1 :::"[#]"::: )  (Set  ($#k1_numbers :::"REAL"::: ) )) ->   ($#v3_rcomp_1 :::"open"::: )   ; 

cluster   ($#v1_xboole_0 :::"empty"::: )    ->   ($#v3_rcomp_1 :::"open"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  ($#k1_numbers :::"REAL"::: ) ))); 
end; registrationlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k2_limfunc1 :::"right_closed_halfline"::: )  "r") ->   ($#v2_rcomp_1 :::"closed"::: )   ; 

cluster (Set   ($#k1_limfunc1 :::"left_closed_halfline"::: )  "r") ->   ($#v2_rcomp_1 :::"closed"::: )   ; 

cluster (Set   ($#k3_limfunc1 :::"right_open_halfline"::: )  "r") ->   ($#v3_rcomp_1 :::"open"::: )   ; 

cluster (Set   ($#k10_prob_1 :::"halfline"::: )  "r") ->   ($#v3_rcomp_1 :::"open"::: )   ; 
end; 
theorem :: FCONT_3:1 (Bool  "for" (Set (Var "g")) "," (Set (Var "x0")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "g"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Set (Var "x0"))  ($#k7_real_1 :::"+"::: )  (Set (Var "r")) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "g"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x0")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))))) ; 
 
theorem :: FCONT_3:2 (Bool  "for" (Set (Var "g")) "," (Set (Var "x0")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "g"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Set (Var "x0"))  ($#k7_real_1 :::"+"::: )  (Set (Var "r")) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) "holds"  (Bool (Set (Set (Var "g"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x0")))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) )))) ; 
 
theorem :: FCONT_3:3 (Bool  "for" (Set (Var "g")) "," (Set (Var "x0")) "," (Set (Var "r1")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x0"))  ($#k7_real_1 :::"+"::: )  (Set (Var "r1")))) & (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "r1")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))) "holds"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))) & (Bool (Set (Var "g"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Set (Var "x0"))  ($#k7_real_1 :::"+"::: )  (Set (Var "r")) ")" ) ($#k2_rcomp_1 :::".["::: ) ))  ")" ))) ; 
 
theorem :: FCONT_3:4 (Bool  "for" (Set (Var "g")) "," (Set (Var "x0")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "g"))  ($#k9_real_1 :::"-"::: )  (Set (Var "x0")))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) ))) "holds"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))) & (Bool (Set (Var "g"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Set (Var "x0"))  ($#k9_real_1 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Set (Var "x0"))  ($#k7_real_1 :::"+"::: )  (Set (Var "r")) ")" ) ($#k2_rcomp_1 :::".["::: ) ))  ")" ))) ; 
 
theorem :: FCONT_3:5 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "x0")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x0"))  ($#k5_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "n"))  ($#k7_real_1 :::"+"::: )  (Num 1) ")" ) ")" )))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "a")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "x0")))  ")" )))) ; 
 
theorem :: FCONT_3:6 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "x0")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x0"))  ($#k3_real_1 :::"+"::: )  (Set  "(" (Set (Var "p"))  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "n"))  ($#k7_real_1 :::"+"::: )  (Num 1) ")" ) ")" )))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "a")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "x0")))  ")" )))) ; 
 
theorem :: FCONT_3:7 (Bool  "for" (Set (Var "x0")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (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"))  ($#r1_fcont_1 :::"is_continuous_in"::: )  (Set (Var "x0"))) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x0")))  ($#r1_hidden :::"<>"::: )  (Set (Var "r"))) & (Bool  "ex" (Set (Var "N")) "being"    ($#m1_rcomp_1 :::"Neighbourhood"::: )   "of" (Set (Var "x0")) "st" (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))))) "holds"  (Bool  "ex" (Set (Var "N")) "being"    ($#m1_rcomp_1 :::"Neighbourhood"::: )   "of" (Set (Var "x0")) "st"  (Bool  "("  (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "g"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "g")))  ($#r1_hidden :::"<>"::: )  (Set (Var "r")))  ")" )  ")" ))))) ; 
 
theorem :: FCONT_3:8 (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  "("  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v5_valued_0 :::"increasing"::: )  ) "or" (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v6_valued_0 :::"decreasing"::: )  )  ")" )) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ))) ; 
 
theorem :: FCONT_3:9 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (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 (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v5_valued_0 :::"increasing"::: )  )) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X")) ")" )  ($#k2_partfun2 :::"""::: )  ")" )  ($#k2_partfun1 :::"|"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "X")) ")" )) "is"   ($#v5_valued_0 :::"increasing"::: )  ))) ; 
 
theorem :: FCONT_3:10 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (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 (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v6_valued_0 :::"decreasing"::: )  )) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X")) ")" )  ($#k2_partfun2 :::"""::: )  ")" )  ($#k2_partfun1 :::"|"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "X")) ")" )) "is"   ($#v6_valued_0 :::"decreasing"::: )  ))) ; 
 
theorem :: FCONT_3:11 (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_rfunct_2 :::"monotone"::: )  ) & (Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_prob_1 :::"left_open_halfline"::: )  (Set (Var "p")))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  ))) ; 
 
theorem :: FCONT_3:12 (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_rfunct_2 :::"monotone"::: )  ) & (Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_limfunc1 :::"right_open_halfline"::: )  (Set (Var "p")))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  ))) ; 
 
theorem :: FCONT_3:13 (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_rfunct_2 :::"monotone"::: )  ) & (Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_limfunc1 :::"left_closed_halfline"::: )  (Set (Var "p")))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  ))) ; 
 
theorem :: FCONT_3: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"   ($#v1_rfunct_2 :::"monotone"::: )  ) & (Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_limfunc1 :::"right_closed_halfline"::: )  (Set (Var "p")))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  ))) ; 
 
theorem :: FCONT_3:15 (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_rfunct_2 :::"monotone"::: )  ) & (Bool  "ex" (Set (Var "p")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  ))) ; 
 
theorem :: FCONT_3:16 (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_rfunct_2 :::"monotone"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  ))) ; 
 
theorem :: FCONT_3:17 (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  "("  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )) "is"   ($#v5_valued_0 :::"increasing"::: )  ) "or" (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )) "is"   ($#v6_valued_0 :::"decreasing"::: )  )  ")" ) & (Bool (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) ) ")" )  ($#k2_partfun2 :::"""::: )  ")" )  ($#k2_partfun1 :::"|"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) ) ")" )) "is"   ($#v1_fcont_1 :::"continuous"::: )  ))) ; 
 
theorem :: FCONT_3:18 (Bool  "for" (Set (Var "p")) "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  "("  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k10_prob_1 :::"left_open_halfline"::: )  (Set (Var "p")) ")" )) "is"   ($#v5_valued_0 :::"increasing"::: )  ) "or" (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k10_prob_1 :::"left_open_halfline"::: )  (Set (Var "p")) ")" )) "is"   ($#v6_valued_0 :::"decreasing"::: )  )  ")" ) & (Bool (Set   ($#k10_prob_1 :::"left_open_halfline"::: )  (Set (Var "p")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k10_prob_1 :::"left_open_halfline"::: )  (Set (Var "p")) ")" ) ")" )  ($#k2_partfun2 :::"""::: )  ")" )  ($#k2_partfun1 :::"|"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k10_prob_1 :::"left_open_halfline"::: )  (Set (Var "p")) ")" ) ")" )) "is"   ($#v1_fcont_1 :::"continuous"::: )  ))) ; 
 
theorem :: FCONT_3:19 (Bool  "for" (Set (Var "p")) "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  "("  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k3_limfunc1 :::"right_open_halfline"::: )  (Set (Var "p")) ")" )) "is"   ($#v5_valued_0 :::"increasing"::: )  ) "or" (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k3_limfunc1 :::"right_open_halfline"::: )  (Set (Var "p")) ")" )) "is"   ($#v6_valued_0 :::"decreasing"::: )  )  ")" ) & (Bool (Set   ($#k3_limfunc1 :::"right_open_halfline"::: )  (Set (Var "p")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k3_limfunc1 :::"right_open_halfline"::: )  (Set (Var "p")) ")" ) ")" )  ($#k2_partfun2 :::"""::: )  ")" )  ($#k2_partfun1 :::"|"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k3_limfunc1 :::"right_open_halfline"::: )  (Set (Var "p")) ")" ) ")" )) "is"   ($#v1_fcont_1 :::"continuous"::: )  ))) ; 
 
theorem :: FCONT_3:20 (Bool  "for" (Set (Var "p")) "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  "("  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k1_limfunc1 :::"left_closed_halfline"::: )  (Set (Var "p")) ")" )) "is"   ($#v5_valued_0 :::"increasing"::: )  ) "or" (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k1_limfunc1 :::"left_closed_halfline"::: )  (Set (Var "p")) ")" )) "is"   ($#v6_valued_0 :::"decreasing"::: )  )  ")" ) & (Bool (Set   ($#k1_limfunc1 :::"left_closed_halfline"::: )  (Set (Var "p")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k1_limfunc1 :::"left_closed_halfline"::: )  (Set (Var "p")) ")" ) ")" )  ($#k2_partfun2 :::"""::: )  ")" )  ($#k2_partfun1 :::"|"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k1_limfunc1 :::"left_closed_halfline"::: )  (Set (Var "p")) ")" ) ")" )) "is"   ($#v1_fcont_1 :::"continuous"::: )  ))) ; 
 
theorem :: FCONT_3:21 (Bool  "for" (Set (Var "p")) "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  "("  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k2_limfunc1 :::"right_closed_halfline"::: )  (Set (Var "p")) ")" )) "is"   ($#v5_valued_0 :::"increasing"::: )  ) "or" (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k2_limfunc1 :::"right_closed_halfline"::: )  (Set (Var "p")) ")" )) "is"   ($#v6_valued_0 :::"decreasing"::: )  )  ")" ) & (Bool (Set   ($#k2_limfunc1 :::"right_closed_halfline"::: )  (Set (Var "p")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k2_limfunc1 :::"right_closed_halfline"::: )  (Set (Var "p")) ")" ) ")" )  ($#k2_partfun2 :::"""::: )  ")" )  ($#k2_partfun1 :::"|"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k2_limfunc1 :::"right_closed_halfline"::: )  (Set (Var "p")) ")" ) ")" )) "is"   ($#v1_fcont_1 :::"continuous"::: )  ))) ; 
 
theorem :: FCONT_3:22 (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  "("  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k2_subset_1 :::"[#]"::: )  (Set  ($#k1_numbers :::"REAL"::: ) ) ")" )) "is"   ($#v5_valued_0 :::"increasing"::: )  ) "or" (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k2_subset_1 :::"[#]"::: )  (Set  ($#k1_numbers :::"REAL"::: ) ) ")" )) "is"   ($#v6_valued_0 :::"decreasing"::: )  )  ")" ) & (Bool (Set (Var "f")) "is"   ($#v1_partfun1 :::"total"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k2_partfun2 :::"""::: )  ")" )  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")) ")" )) "is"   ($#v1_fcont_1 :::"continuous"::: )  )) ; 
 
theorem :: FCONT_3:23 (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  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )) "is"   ($#v5_valued_0 :::"increasing"::: )  ) "or" (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) )) "is"   ($#v6_valued_0 :::"decreasing"::: )  )  ")" )) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set  "(" (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k2_rcomp_1 :::".["::: ) ) ")" )) "is"   ($#v3_rcomp_1 :::"open"::: )  ))) ; 
 
theorem :: FCONT_3:24 (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   ($#k10_prob_1 :::"left_open_halfline"::: )  (Set (Var "p")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k10_prob_1 :::"left_open_halfline"::: )  (Set (Var "p")) ")" )) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k10_prob_1 :::"left_open_halfline"::: )  (Set (Var "p")) ")" )) "is"   ($#v5_valued_0 :::"increasing"::: )  ) "or" (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k10_prob_1 :::"left_open_halfline"::: )  (Set (Var "p")) ")" )) "is"   ($#v6_valued_0 :::"decreasing"::: )  )  ")" )) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set  "(" (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k10_prob_1 :::"left_open_halfline"::: )  (Set (Var "p")) ")" ) ")" )) "is"   ($#v3_rcomp_1 :::"open"::: )  ))) ; 
 
theorem :: FCONT_3:25 (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   ($#k3_limfunc1 :::"right_open_halfline"::: )  (Set (Var "p")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k3_limfunc1 :::"right_open_halfline"::: )  (Set (Var "p")) ")" )) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k3_limfunc1 :::"right_open_halfline"::: )  (Set (Var "p")) ")" )) "is"   ($#v5_valued_0 :::"increasing"::: )  ) "or" (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k3_limfunc1 :::"right_open_halfline"::: )  (Set (Var "p")) ")" )) "is"   ($#v6_valued_0 :::"decreasing"::: )  )  ")" )) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set  "(" (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k3_limfunc1 :::"right_open_halfline"::: )  (Set (Var "p")) ")" ) ")" )) "is"   ($#v3_rcomp_1 :::"open"::: )  ))) ; 
 
theorem :: FCONT_3:26 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k2_subset_1 :::"[#]"::: )  (Set  ($#k1_numbers :::"REAL"::: ) ))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k2_subset_1 :::"[#]"::: )  (Set  ($#k1_numbers :::"REAL"::: ) ) ")" )) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k2_subset_1 :::"[#]"::: )  (Set  ($#k1_numbers :::"REAL"::: ) ) ")" )) "is"   ($#v5_valued_0 :::"increasing"::: )  ) "or" (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k2_subset_1 :::"[#]"::: )  (Set  ($#k1_numbers :::"REAL"::: ) ) ")" )) "is"   ($#v6_valued_0 :::"decreasing"::: )  )  ")" )) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f"))) "is"   ($#v3_rcomp_1 :::"open"::: )  )) ;