:: RCOMP_3  semantic presentation begin  registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k2_subset_1 :::"[#]"::: )  "X") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; registration
cluster   ->   ($#v3_topmetr :::"real-membered"::: )    for    ($#m1_topmetr :::"SubSpace"::: )   "of" (Set   ($#k8_metric_1 :::"RealSpace"::: )  ); 
end; 
theorem :: RCOMP_3:1 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_membered :::"real-membered"::: )     ($#v3_xxreal_2 :::"bounded_below"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"   ($#v2_rcomp_1 :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool (Set   ($#k3_seq_4 :::"lower_bound"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))))) ; 
 
theorem :: RCOMP_3:2 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_membered :::"real-membered"::: )     ($#v4_xxreal_2 :::"bounded_above"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "being"   ($#v2_rcomp_1 :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool (Set   ($#k2_seq_4 :::"upper_bound"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))))) ; 
 
theorem :: RCOMP_3:3 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k6_measure6 :::"Cl"::: )  (Set  "(" (Set (Var "X"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_measure6 :::"Cl"::: )  (Set (Var "X")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k6_measure6 :::"Cl"::: )  (Set (Var "Y")) ")" )))) ; 
 begin  





registrationlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "s" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set  ($#k2_xxreal_1 :::"[."::: ) "r" "," "s" ($#k2_xxreal_1 :::".["::: ) ) ->   ($#v3_xxreal_2 :::"bounded_below"::: )   ; 

cluster (Set  ($#k3_xxreal_1 :::"]."::: ) "s" "," "r" ($#k3_xxreal_1 :::".]"::: ) ) ->   ($#v4_xxreal_2 :::"bounded_above"::: )   ; 
end; registrationlet "r", "s" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set  ($#k2_xxreal_1 :::"[."::: ) "r" "," "s" ($#k2_xxreal_1 :::".["::: ) ) ->   ($#v5_xxreal_2 :::"real-bounded"::: )   ; 

cluster (Set  ($#k3_xxreal_1 :::"]."::: ) "r" "," "s" ($#k3_xxreal_1 :::".]"::: ) ) ->   ($#v5_xxreal_2 :::"real-bounded"::: )   ; 

cluster (Set  ($#k4_xxreal_1 :::"]."::: ) "r" "," "s" ($#k4_xxreal_1 :::".["::: ) ) ->   ($#v5_xxreal_2 :::"real-bounded"::: )   ; 
end; registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_membered :::"complex-membered"::: )     ($#v2_membered :::"ext-real-membered"::: )     ($#v3_membered :::"real-membered"::: )     ($#v3_rcomp_1 :::"open"::: )     ($#v5_xxreal_2 :::"real-bounded"::: )     ($#v6_xxreal_2 :::"interval"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  ($#k1_numbers :::"REAL"::: ) ))); 
end; 
theorem :: RCOMP_3:4 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s")))) "holds"  (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  ($#k3_rcomp_1 :::"[."::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k3_rcomp_1 :::".["::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "r")))) ; 
 
theorem :: RCOMP_3:5 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s")))) "holds"  (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  ($#k3_rcomp_1 :::"[."::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k3_rcomp_1 :::".["::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "s")))) ; 
 
theorem :: RCOMP_3:6 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s")))) "holds"  (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  ($#k4_rcomp_1 :::"]."::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k4_rcomp_1 :::".]"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "r")))) ; 
 
theorem :: RCOMP_3:7 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s")))) "holds"  (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  ($#k4_rcomp_1 :::"]."::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k4_rcomp_1 :::".]"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "s")))) ; 
 begin  
theorem :: RCOMP_3:8 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "holds"  (Bool (Set (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set  "("  ($#k1_limfunc1 :::"left_closed_halfline"::: )  (Set (Var "a")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_limfunc1 :::"right_closed_halfline"::: )  (Set (Var "b")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) ))) ; 
 registrationlet "a" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k1_limfunc1 :::"left_closed_halfline"::: )  "a") ->  ($#~v3_xxreal_2  "non"   ($#v3_xxreal_2 :::"bounded_below"::: )   )    ($#v4_xxreal_2 :::"bounded_above"::: )     ($#v6_xxreal_2 :::"interval"::: )   ; 

cluster (Set   ($#k10_prob_1 :::"left_open_halfline"::: )  "a") ->  ($#~v3_xxreal_2  "non"   ($#v3_xxreal_2 :::"bounded_below"::: )   )    ($#v4_xxreal_2 :::"bounded_above"::: )     ($#v6_xxreal_2 :::"interval"::: )   ; 

cluster (Set   ($#k2_limfunc1 :::"right_closed_halfline"::: )  "a") ->   ($#v3_xxreal_2 :::"bounded_below"::: )    ($#~v4_xxreal_2  "non"   ($#v4_xxreal_2 :::"bounded_above"::: )   )    ($#v6_xxreal_2 :::"interval"::: )   ; 

cluster (Set   ($#k3_limfunc1 :::"right_open_halfline"::: )  "a") ->   ($#v3_xxreal_2 :::"bounded_below"::: )    ($#~v4_xxreal_2  "non"   ($#v4_xxreal_2 :::"bounded_above"::: )   )    ($#v6_xxreal_2 :::"interval"::: )   ; 
end; 
theorem :: RCOMP_3:9 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "("  ($#k1_limfunc1 :::"left_closed_halfline"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: RCOMP_3:10 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "("  ($#k10_prob_1 :::"left_open_halfline"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: RCOMP_3:11 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  "("  ($#k2_limfunc1 :::"right_closed_halfline"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: RCOMP_3:12 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  "("  ($#k3_limfunc1 :::"right_open_halfline"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 begin  registration
cluster (Set   ($#k2_subset_1 :::"[#]"::: )  (Set  ($#k1_numbers :::"REAL"::: ) )) ->  ($#~v3_xxreal_2  "non"   ($#v3_xxreal_2 :::"bounded_below"::: )   )   ($#~v4_xxreal_2  "non"   ($#v4_xxreal_2 :::"bounded_above"::: )   )    ($#v6_xxreal_2 :::"interval"::: )   ; 
end; 
theorem :: RCOMP_3:13 (Bool  "for" (Set (Var "X")) "being"   ($#v5_xxreal_2 :::"real-bounded"::: )     ($#v6_xxreal_2 :::"interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "X")) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) ; 
 
theorem :: RCOMP_3:14 (Bool  "for" (Set (Var "X")) "being"   ($#v5_xxreal_2 :::"real-bounded"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Bool  "not" (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set  ($#k4_rcomp_1 :::"]."::: ) (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "X")) ")" ) ($#k4_rcomp_1 :::".]"::: ) ))) ; 
 
theorem :: RCOMP_3:15 (Bool  "for" (Set (Var "X")) "being"   ($#v5_xxreal_2 :::"real-bounded"::: )     ($#v6_xxreal_2 :::"interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Bool  "not" (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) & (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_rcomp_1 :::"]."::: ) (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "X")) ")" ) ($#k4_rcomp_1 :::".]"::: ) ))) ; 
 
theorem :: RCOMP_3:16 (Bool  "for" (Set (Var "X")) "being"   ($#v5_xxreal_2 :::"real-bounded"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Bool  "not" (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set  ($#k3_rcomp_1 :::"[."::: ) (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "X")) ")" ) ($#k3_rcomp_1 :::".["::: ) ))) ; 
 
theorem :: RCOMP_3:17 (Bool  "for" (Set (Var "X")) "being"   ($#v5_xxreal_2 :::"real-bounded"::: )     ($#v6_xxreal_2 :::"interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Bool  "not" (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k3_rcomp_1 :::"[."::: ) (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "X")) ")" ) ($#k3_rcomp_1 :::".["::: ) ))) ; 
 
theorem :: RCOMP_3:18 (Bool  "for" (Set (Var "X")) "being"   ($#v5_xxreal_2 :::"real-bounded"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Bool  "not" (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) & (Bool (Bool  "not" (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "X")) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) ; 
 
theorem :: RCOMP_3:19 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v5_xxreal_2 :::"real-bounded"::: )     ($#v6_xxreal_2 :::"interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Bool  "not" (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) & (Bool (Bool  "not" (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "X")) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) ; 
 
theorem :: RCOMP_3:20 (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v4_xxreal_2 :::"bounded_above"::: )  )) "holds"  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_limfunc1 :::"left_closed_halfline"::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "X")) ")" )))) ; 
 
theorem :: RCOMP_3:21 (Bool  "for" (Set (Var "X")) "being"   ($#v6_xxreal_2 :::"interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Bool  "not" (Set (Var "X")) "is"   ($#v3_xxreal_2 :::"bounded_below"::: )  )) & (Bool (Set (Var "X")) "is"   ($#v4_xxreal_2 :::"bounded_above"::: )  ) & (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_limfunc1 :::"left_closed_halfline"::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "X")) ")" )))) ; 
 
theorem :: RCOMP_3:22 (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v4_xxreal_2 :::"bounded_above"::: )  ) & (Bool (Bool  "not" (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k10_prob_1 :::"left_open_halfline"::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "X")) ")" )))) ; 
 
theorem :: RCOMP_3:23 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v6_xxreal_2 :::"interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Bool  "not" (Set (Var "X")) "is"   ($#v3_xxreal_2 :::"bounded_below"::: )  )) & (Bool (Set (Var "X")) "is"   ($#v4_xxreal_2 :::"bounded_above"::: )  ) & (Bool (Bool  "not" (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_prob_1 :::"left_open_halfline"::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "X")) ")" )))) ; 
 
theorem :: RCOMP_3:24 (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v3_xxreal_2 :::"bounded_below"::: )  )) "holds"  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_limfunc1 :::"right_closed_halfline"::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X")) ")" )))) ; 
 
theorem :: RCOMP_3:25 (Bool  "for" (Set (Var "X")) "being"   ($#v6_xxreal_2 :::"interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v3_xxreal_2 :::"bounded_below"::: )  ) & (Bool (Bool  "not" (Set (Var "X")) "is"   ($#v4_xxreal_2 :::"bounded_above"::: )  )) & (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_limfunc1 :::"right_closed_halfline"::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X")) ")" )))) ; 
 
theorem :: RCOMP_3:26 (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v3_xxreal_2 :::"bounded_below"::: )  ) & (Bool (Bool  "not" (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_limfunc1 :::"right_open_halfline"::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X")) ")" )))) ; 
 
theorem :: RCOMP_3:27 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v6_xxreal_2 :::"interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v3_xxreal_2 :::"bounded_below"::: )  ) & (Bool (Bool  "not" (Set (Var "X")) "is"   ($#v4_xxreal_2 :::"bounded_above"::: )  )) & (Bool (Bool  "not" (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_limfunc1 :::"right_open_halfline"::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X")) ")" )))) ; 
 
theorem :: RCOMP_3:28 (Bool  "for" (Set (Var "X")) "being"   ($#v6_xxreal_2 :::"interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Bool  "not" (Set (Var "X")) "is"   ($#v4_xxreal_2 :::"bounded_above"::: )  )) & (Bool (Bool  "not" (Set (Var "X")) "is"   ($#v3_xxreal_2 :::"bounded_below"::: )  ))) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))) ; 
 
theorem :: RCOMP_3:29 (Bool  "for" (Set (Var "X")) "being"   ($#v6_xxreal_2 :::"interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "holds"  (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v1_xboole_0 :::"empty"::: )  ) "or" (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_numbers :::"REAL"::: )  )) "or" (Bool  "ex" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st" (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_limfunc1 :::"left_closed_halfline"::: )  (Set (Var "a"))))) "or" (Bool  "ex" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st" (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_prob_1 :::"left_open_halfline"::: )  (Set (Var "a"))))) "or" (Bool  "ex" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st" (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_limfunc1 :::"right_closed_halfline"::: )  (Set (Var "a"))))) "or" (Bool  "ex" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st" (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_limfunc1 :::"right_open_halfline"::: )  (Set (Var "a"))))) "or" (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))  ")" )) "or" (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k3_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_rcomp_1 :::".["::: ) ))  ")" )) "or" (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_rcomp_1 :::".]"::: ) ))  ")" )) "or" (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ))  ")" ))  ")" )) ; 
 
theorem :: RCOMP_3:30 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v6_xxreal_2 :::"interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "holds"  (Bool  "("  (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) "or" (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X")))) "or" (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "X")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))  ")" ))) ; 
 
theorem :: RCOMP_3:31 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v5_xxreal_2 :::"real-bounded"::: )     ($#v6_xxreal_2 :::"interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "Y")))) & (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "Y")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "X")))) &  "("  (Bool (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "Y")))) & (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "Y")))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))) "implies" (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  ")"  &  "("  (Bool (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "Y")))) & (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "Y")))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))) "implies" (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  ")" ) "holds"  (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))) ; 
 registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_membered :::"complex-membered"::: )     ($#v2_membered :::"ext-real-membered"::: )     ($#v3_membered :::"real-membered"::: )     ($#v2_rcomp_1 :::"closed"::: )     ($#v3_rcomp_1 :::"open"::: )    ($#~v5_xxreal_2  "non"   ($#v5_xxreal_2 :::"real-bounded"::: )   )    ($#v6_xxreal_2 :::"interval"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  ($#k1_numbers :::"REAL"::: ) ))); 
end; begin  
theorem :: RCOMP_3:32 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_topalg_2 :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_tops_1 :::"Fr"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) )))) ; 
 
theorem :: RCOMP_3:33 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_topalg_2 :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ))) "holds"  (Bool (Set   ($#k2_tops_1 :::"Fr"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) )))) ; 
 
theorem :: RCOMP_3:34 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_topalg_2 :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k3_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_rcomp_1 :::".["::: ) ))) "holds"  (Bool (Set   ($#k2_tops_1 :::"Fr"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) )))) ; 
 
theorem :: RCOMP_3:35 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_topalg_2 :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_tops_1 :::"Fr"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) )))) ; 
 
theorem :: RCOMP_3:36 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_topalg_2 :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) )))) ; 
 
theorem :: RCOMP_3:37 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_topalg_2 :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ))) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) )))) ; 
 
theorem :: RCOMP_3:38 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_topalg_2 :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k3_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_rcomp_1 :::".["::: ) ))) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) )))) ; 
 
theorem :: RCOMP_3:39 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_topalg_2 :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) )))) ; 
 registrationlet "T" be   ($#v3_topmetr :::"real-membered"::: )     ($#l1_pre_topc :::"TopStruct"::: )  ; let "X" be   ($#v6_xxreal_2 :::"interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); 
cluster (Set "T"  ($#k1_pre_topc :::"|"::: )  "X") ->   ($#v2_topalg_2 :::"interval"::: )   ; 
end; registrationlet "A" be   ($#v6_xxreal_2 :::"interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ); 
cluster (Set   ($#k5_toprealb :::"R^1"::: )  "A") ->   ($#v6_xxreal_2 :::"interval"::: )   ; 
end; registration
cluster   ($#v2_connsp_1 :::"connected"::: )    ->   ($#v6_xxreal_2 :::"interval"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k2_topalg_2 :::"R^1"::: ) )))); 

cluster   ($#v6_xxreal_2 :::"interval"::: )    ->   ($#v2_connsp_1 :::"connected"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k2_topalg_2 :::"R^1"::: ) )))); 
end; begin  registrationlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" "r" "," "r" ")" ) -> (Num 1)  ($#v13_struct_0 :::"-element"::: )   ; 
end; 
theorem :: RCOMP_3:40 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))) "holds"  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" ) "holds"  (Bool (Set (Var "A")) "is"   ($#v5_xxreal_2 :::"real-bounded"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )))) ; 
 
theorem :: RCOMP_3:41 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))) "holds"  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )  "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k3_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_rcomp_1 :::".["::: ) )) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) )))) ; 
 
theorem :: RCOMP_3:42 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))) "holds"  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )  "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_rcomp_1 :::".]"::: ) )) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s")))) "holds"  (Bool (Set   ($#k1_tops_1 :::"Int"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) )))) ; 
 
theorem :: RCOMP_3:43 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Var "Y")))) "holds"  (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v2_connsp_1 :::"connected"::: )  ) "iff" (Bool (Set (Var "Y")) "is"   ($#v6_xxreal_2 :::"interval"::: )  )  ")" )))) ; 
 registrationlet "T" be   ($#l1_pre_topc :::"TopSpace":::); 
cluster   ($#v3_pre_topc :::"open"::: )     ($#v4_pre_topc :::"closed"::: )     ($#v2_connsp_1 :::"connected"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T"))); 
end; registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_connsp_1 :::"connected"::: )    ($#l1_pre_topc :::"TopSpace":::); 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_pre_topc :::"open"::: )     ($#v4_pre_topc :::"closed"::: )     ($#v2_connsp_1 :::"connected"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T"))); 
end; 
theorem :: RCOMP_3:44 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))) "holds"  (Bool  "for" (Set (Var "X")) "being"   ($#v3_pre_topc :::"open"::: )     ($#v2_connsp_1 :::"connected"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )  "holds"  (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v1_xboole_0 :::"empty"::: )  ) "or" (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k1_rcomp_1 :::".]"::: ) )) "or" (Bool  "ex" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s"))) & (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k3_rcomp_1 :::"[."::: ) (Set (Var "r")) "," (Set (Var "a")) ($#k3_rcomp_1 :::".["::: ) ))  ")" )) "or" (Bool  "ex" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s"))) & (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "s")) ($#k4_rcomp_1 :::".]"::: ) ))  ")" )) "or" (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s"))) & (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ))  ")" ))  ")" ))) ; 
 begin  
theorem :: RCOMP_3:45 (Bool  "for" (Set (Var "T")) "being"    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "F1")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "T"))) & (Bool (Set (Var "F1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k7_subset_1 :::"\"::: )   "{"  (Set (Var "X")) where X "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool  "("  (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "F"))) & (Bool  "ex" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st"  (Bool  "("  (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set (Var "F"))) & (Bool (Set (Var "X"))  ($#r2_xboole_0 :::"c<"::: )  (Set (Var "Y")))  ")" ))  ")" )  "}"  ))) "holds"  (Bool (Set (Var "F1")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "T")))))) ; 
 
theorem :: RCOMP_3:46 (Bool  "for" (Set (Var "S")) "being" (Num 1)  ($#v13_struct_0 :::"-element"::: )     ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "S")))) "holds"  (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "s")) ($#k1_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "F")))))) ; 
 definitionlet "T" be    ($#l1_pre_topc :::"TopStruct"::: )  ; let "F" be   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "T")); attr "F" is  :::"connected":::  means :: RCOMP_3:def 1 (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "T"  "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  "F")) "holds"  (Bool (Set (Var "X")) "is"   ($#v2_connsp_1 :::"connected"::: )  )); end; 





:: deftheorem    defines :::"connected"::: RCOMP_3:def 1 :  (Bool  "for" (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v1_rcomp_3 :::"connected"::: )  ) "iff" (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))) "holds"  (Bool (Set (Var "X")) "is"   ($#v2_connsp_1 :::"connected"::: )  ))  ")" ))); 
 registrationlet "T" be   ($#l1_pre_topc :::"TopSpace":::); 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_tops_2 :::"open"::: )     ($#v2_tops_2 :::"closed"::: )     ($#v1_rcomp_3 :::"connected"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK1_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T"))))); 
end; 







theorem :: RCOMP_3:47 (Bool  "for" (Set (Var "L")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "G")) "," (Set (Var "G1")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "G")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "L"))) & (Bool (Set (Var "G")) "is"   ($#v1_finset_1 :::"finite"::: )  )) "holds"  (Bool  "for" (Set (Var "ALL")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "G1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k7_subset_1 :::"\"::: )   "{"  (Set (Var "X")) where X "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) : (Bool  "("  (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "G"))) & (Bool  "ex" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "st"  (Bool  "("  (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set (Var "G"))) & (Bool (Set (Var "X"))  ($#r2_xboole_0 :::"c<"::: )  (Set (Var "Y")))  ")" ))  ")" )  "}"  )) & (Bool (Set (Var "ALL"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "C")) where C "is"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "L")) : (Bool  "("  (Bool (Set (Var "C")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "L"))) & (Bool (Set (Var "C"))  ($#r1_tarski :::"c="::: )  (Set (Var "G1")))  ")" )  "}"  )) "holds"  (Bool (Set (Var "ALL"))  ($#r5_orders_1 :::"has_lower_Zorn_property_wrt"::: )  (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "ALL"))))))) ; 
 
theorem :: RCOMP_3:48 (Bool  "for" (Set (Var "L")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "G")) "," (Set (Var "ALL")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "ALL"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "C")) where C "is"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "L")) : (Bool  "("  (Bool (Set (Var "C")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "L"))) & (Bool (Set (Var "C"))  ($#r1_tarski :::"c="::: )  (Set (Var "G")))  ")" )  "}"  )) "holds"  (Bool  "for" (Set (Var "M")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "M"))  ($#r7_orders_1 :::"is_minimal_in"::: )  (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "ALL")))) & (Bool (Set (Var "M"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "ALL")) ")" )))) "holds"  (Bool  "for" (Set (Var "A1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "A1"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) "holds"  (Bool  "for" (Set (Var "A2")) "," (Set (Var "A3")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L"))  "holds"  (Bool  "("   "not" (Bool (Set (Var "A2"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) "or"  "not" (Bool (Set (Var "A3"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) "or"  "not" (Bool (Set (Var "A1"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A2"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "A3")))) "or"  "not" (Bool (Set (Var "A1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "A2"))) "or"  "not" (Bool (Set (Var "A1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "A3")))  ")" )))))) ; 
 definitionlet "r", "s" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "F" be   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Const "r")) "," (Set (Const "s")) ")"  ")" ); assume that  
(Bool (Set (Const "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Const "r")) "," (Set (Const "s")) ")"  ")" ))
 and  
(Bool (Set (Const "F")) "is"   ($#v1_tops_2 :::"open"::: )  )
 and  
(Bool (Set (Const "F")) "is"   ($#v1_rcomp_3 :::"connected"::: )  )
 and  
(Bool (Set (Const "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Const "s")))
 ; mode  :::"IntervalCover":::  "of" "F" ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k9_setfam_1 :::"bool"::: )  (Set  ($#k1_numbers :::"REAL"::: ) )) means :: RCOMP_3:def 2 (Bool  "("  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  it)  ($#r1_tarski :::"c="::: )  "F") & (Bool (Set   ($#k5_setfam_1 :::"union"::: )  (Set  "("  ($#k2_relset_1 :::"rng"::: )  it ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) "r" "," "s" ($#k1_rcomp_1 :::".]"::: ) )) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  it))) "implies" (Bool  "not" (Bool (Set it  ($#k7_partfun1 :::"/."::: )  (Set (Var "n"))) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  it))) "implies" (Bool  "("  (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  "(" it  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  "(" it  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))) & (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "(" it  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "(" it  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))) & (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  "(" it  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "(" it  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" )))  ")" )  ")"  &  "("  (Bool (Bool (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  it))) "implies" (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "(" it  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  "(" it  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ) ")" )))  ")"   ")" )  ")" ) &  "("  (Bool (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) "r" "," "s" ($#k1_rcomp_1 :::".]"::: ) )  ($#r2_hidden :::"in"::: )  "F")) "implies" (Bool it  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k1_rcomp_1 :::"[."::: ) "r" "," "s" ($#k1_rcomp_1 :::".]"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set  ($#k1_rcomp_1 :::"[."::: ) "r" "," "s" ($#k1_rcomp_1 :::".]"::: ) )  ($#r2_hidden :::"in"::: )  "F"))) "implies" (Bool  "("  (Bool  "ex" (Set (Var "p")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool "r"  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "p"))) & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  "s") & (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set  ($#k3_rcomp_1 :::"[."::: ) "r" "," (Set (Var "p")) ($#k3_rcomp_1 :::".["::: ) ))  ")" )) & (Bool  "ex" (Set (Var "p")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool "r"  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "p"))) & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<"::: )  "s") & (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  it ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k4_rcomp_1 :::"]."::: ) (Set (Var "p")) "," "s" ($#k4_rcomp_1 :::".]"::: ) ))  ")" )) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  it))) "holds"  (Bool  "ex" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool "r"  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "p"))) & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "q"))) & (Bool (Set (Var "q"))  ($#r1_xxreal_0 :::"<="::: )  "s") & (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k2_rcomp_1 :::".["::: ) ))  ")" ))  ")" )  ")" )  ")"   ")" ); end; 








:: deftheorem    defines :::"IntervalCover"::: RCOMP_3:def 2 :  (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )  "st" (Bool (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )) & (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "F")) "is"   ($#v1_rcomp_3 :::"connected"::: )  ) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))) "holds"  (Bool  "for" (Set (Var "b4")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k9_setfam_1 :::"bool"::: )  (Set  ($#k1_numbers :::"REAL"::: ) )) "holds"   (Bool  "("  (Bool (Set (Var "b4")) "is"    ($#m1_rcomp_3 :::"IntervalCover"::: )   "of" (Set (Var "F"))) "iff" (Bool  "("  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "b4")))  ($#r1_tarski :::"c="::: )  (Set (Var "F"))) & (Bool (Set   ($#k5_setfam_1 :::"union"::: )  (Set  "("  ($#k2_relset_1 :::"rng"::: )  (Set (Var "b4")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b4"))))) "implies" (Bool  "not" (Bool (Set (Set (Var "b4"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n"))) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b4"))))) "implies" (Bool  "("  (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  "(" (Set (Var "b4"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  "(" (Set (Var "b4"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))) & (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "(" (Set (Var "b4"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "(" (Set (Var "b4"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))) & (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  "(" (Set (Var "b4"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "(" (Set (Var "b4"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" )))  ")" )  ")"  &  "("  (Bool (Bool (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b4"))))) "implies" (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "(" (Set (Var "b4"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  "(" (Set (Var "b4"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 2) ")" ) ")" )))  ")"   ")" )  ")" ) &  "("  (Bool (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "F")))) "implies" (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k1_rcomp_1 :::".]"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "F"))))) "implies" (Bool  "("  (Bool  "ex" (Set (Var "p")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "p"))) & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s"))) & (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set  ($#k3_rcomp_1 :::"[."::: ) (Set (Var "r")) "," (Set (Var "p")) ($#k3_rcomp_1 :::".["::: ) ))  ")" )) & (Bool  "ex" (Set (Var "p")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "p"))) & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s"))) & (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "b4")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k4_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "s")) ($#k4_rcomp_1 :::".]"::: ) ))  ")" )) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b4"))))) "holds"  (Bool  "ex" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "p"))) & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "q"))) & (Bool (Set (Var "q"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s"))) & (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k2_rcomp_1 :::".["::: ) ))  ")" ))  ")" )  ")" )  ")"   ")" )  ")" )))); 
 
theorem :: RCOMP_3:49 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )  "st" (Bool (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )) & (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "F")) "is"   ($#v1_rcomp_3 :::"connected"::: )  ) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s"))) & (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k1_rcomp_1 :::".]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "F")))) "holds"  (Bool (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k1_rcomp_1 :::".]"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) "is"    ($#m1_rcomp_3 :::"IntervalCover"::: )   "of" (Set (Var "F"))))) ; 
 



theorem :: RCOMP_3:50 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "r")) ")"  ")" )  (Bool  "for" (Set (Var "C")) "being"    ($#m1_rcomp_3 :::"IntervalCover"::: )   "of" (Set (Var "F"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "r")) ")"  ")" )) & (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "F")) "is"   ($#v1_rcomp_3 :::"connected"::: )  )) "holds"  (Bool (Set (Var "C"))  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "r")) "," (Set (Var "r")) ($#k1_rcomp_1 :::".]"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ))))) ; 
 
theorem :: RCOMP_3:51 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )  (Bool  "for" (Set (Var "C")) "being"    ($#m1_rcomp_3 :::"IntervalCover"::: )   "of" (Set (Var "F"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )) & (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "F")) "is"   ($#v1_rcomp_3 :::"connected"::: )  ) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))) "holds"  (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "C"))))))) ; 
 
theorem :: RCOMP_3:52 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )  (Bool  "for" (Set (Var "C")) "being"    ($#m1_rcomp_3 :::"IntervalCover"::: )   "of" (Set (Var "F"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )) & (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "F")) "is"   ($#v1_rcomp_3 :::"connected"::: )  ) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s"))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Var "C"))  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k1_rcomp_1 :::".]"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ))))) ; 
 
theorem :: RCOMP_3:53 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )  (Bool  "for" (Set (Var "C")) "being"    ($#m1_rcomp_3 :::"IntervalCover"::: )   "of" (Set (Var "F"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )) & (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "F")) "is"   ($#v1_rcomp_3 :::"connected"::: )  ) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s"))) & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "C")))) & (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "C")))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m")))) "holds"  (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  "(" (Set (Var "C"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  "(" (Set (Var "C"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "m")) ")" ))))))) ; 
 
theorem :: RCOMP_3:54 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )  (Bool  "for" (Set (Var "C")) "being"    ($#m1_rcomp_3 :::"IntervalCover"::: )   "of" (Set (Var "F"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )) & (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "F")) "is"   ($#v1_rcomp_3 :::"connected"::: )  ) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s"))) & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "C")))) & (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "C")))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m")))) "holds"  (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "(" (Set (Var "C"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "(" (Set (Var "C"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "m")) ")" ))))))) ; 
 
theorem :: RCOMP_3:55 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )  (Bool  "for" (Set (Var "C")) "being"    ($#m1_rcomp_3 :::"IntervalCover"::: )   "of" (Set (Var "F"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )) & (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "F")) "is"   ($#v1_rcomp_3 :::"connected"::: )  ) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s"))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "C"))))) "holds"  (Bool  "not" (Bool (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set  "(" (Set (Var "C"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" ) "," (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set  "(" (Set (Var "C"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" ) ")" ) ($#k2_rcomp_1 :::".["::: ) ) "is"   ($#v1_xboole_0 :::"empty"::: )  )))))) ; 
 
theorem :: RCOMP_3:56 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )  (Bool  "for" (Set (Var "C")) "being"    ($#m1_rcomp_3 :::"IntervalCover"::: )   "of" (Set (Var "F"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )) & (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "F")) "is"   ($#v1_rcomp_3 :::"connected"::: )  ) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))) "holds"  (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  "(" (Set (Var "C"))  ($#k7_partfun1 :::"/."::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "r")))))) ; 
 
theorem :: RCOMP_3:57 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )  (Bool  "for" (Set (Var "C")) "being"    ($#m1_rcomp_3 :::"IntervalCover"::: )   "of" (Set (Var "F"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )) & (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "F")) "is"   ($#v1_rcomp_3 :::"connected"::: )  ) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))) "holds"  (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "C"))  ($#k7_partfun1 :::"/."::: )  (Num 1)))))) ; 
 
theorem :: RCOMP_3:58 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )  (Bool  "for" (Set (Var "C")) "being"    ($#m1_rcomp_3 :::"IntervalCover"::: )   "of" (Set (Var "F"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )) & (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "F")) "is"   ($#v1_rcomp_3 :::"connected"::: )  ) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))) "holds"  (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "(" (Set (Var "C"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "C")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "s")))))) ; 
 
theorem :: RCOMP_3:59 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )  (Bool  "for" (Set (Var "C")) "being"    ($#m1_rcomp_3 :::"IntervalCover"::: )   "of" (Set (Var "F"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )) & (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "F")) "is"   ($#v1_rcomp_3 :::"connected"::: )  ) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))) "holds"  (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "C"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "C")) ")" )))))) ; 
 definitionlet "r", "s" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "F" be   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Const "r")) "," (Set (Const "s")) ")"  ")" ); let "C" be    ($#m1_rcomp_3 :::"IntervalCover"::: )   "of" (Set (Const "F")); assume 
(Bool  "("  (Bool (Set (Const "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Const "r")) "," (Set (Const "s")) ")"  ")" )) & (Bool (Set (Const "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Const "F")) "is"   ($#v1_rcomp_3 :::"connected"::: )  ) & (Bool (Set (Const "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Const "s")))  ")" )
 ; mode  :::"IntervalCoverPts":::  "of" "C" ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) means :: RCOMP_3:def 3 (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  it)  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_finseq_1 :::"len"::: )  "C" ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  "r") & (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  it ")" ))  ($#r1_hidden :::"="::: )  "s") & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  it))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set  "(" "C"  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" ) "," (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set  "(" "C"  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" ) ")" ) ($#k2_rcomp_1 :::".["::: ) ))  ")" )  ")" ); end; 









:: deftheorem    defines :::"IntervalCoverPts"::: RCOMP_3:def 3 :  (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )  (Bool  "for" (Set (Var "C")) "being"    ($#m1_rcomp_3 :::"IntervalCover"::: )   "of" (Set (Var "F"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )) & (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "F")) "is"   ($#v1_rcomp_3 :::"connected"::: )  ) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))) "holds"  (Bool  "for" (Set (Var "b5")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b5")) "is"    ($#m2_rcomp_3 :::"IntervalCoverPts"::: )   "of" (Set (Var "C"))) "iff" (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b5")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "C")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool (Set (Set (Var "b5"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "r"))) & (Bool (Set (Set (Var "b5"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "b5")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "s"))) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b5"))))) "holds"  (Bool (Set (Set (Var "b5"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set  "(" (Set (Var "C"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" ) "," (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set  "(" (Set (Var "C"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" ) ")" ) ($#k2_rcomp_1 :::".["::: ) ))  ")" )  ")" )  ")" ))))); 
 



theorem :: RCOMP_3:60 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )  (Bool  "for" (Set (Var "C")) "being"    ($#m1_rcomp_3 :::"IntervalCover"::: )   "of" (Set (Var "F"))  (Bool  "for" (Set (Var "G")) "being"    ($#m2_rcomp_3 :::"IntervalCoverPts"::: )   "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )) & (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "F")) "is"   ($#v1_rcomp_3 :::"connected"::: )  ) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))) "holds"  (Bool (Num 2)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G")))))))) ; 
 
theorem :: RCOMP_3:61 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )  (Bool  "for" (Set (Var "C")) "being"    ($#m1_rcomp_3 :::"IntervalCover"::: )   "of" (Set (Var "F"))  (Bool  "for" (Set (Var "G")) "being"    ($#m2_rcomp_3 :::"IntervalCoverPts"::: )   "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )) & (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "F")) "is"   ($#v1_rcomp_3 :::"connected"::: )  ) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s"))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Var "G"))  ($#r1_hidden :::"="::: )  (Set  ($#k10_finseq_1 :::"<*"::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k10_finseq_1 :::"*>"::: ) )))))) ; 
 
theorem :: RCOMP_3:62 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )  (Bool  "for" (Set (Var "C")) "being"    ($#m1_rcomp_3 :::"IntervalCover"::: )   "of" (Set (Var "F"))  (Bool  "for" (Set (Var "G")) "being"    ($#m2_rcomp_3 :::"IntervalCoverPts"::: )   "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )) & (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "F")) "is"   ($#v1_rcomp_3 :::"connected"::: )  ) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s"))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G"))))) "holds"  (Bool (Set (Set (Var "G"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "(" (Set (Var "C"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" )))))))) ; 
 
theorem :: RCOMP_3:63 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )  (Bool  "for" (Set (Var "C")) "being"    ($#m1_rcomp_3 :::"IntervalCover"::: )   "of" (Set (Var "F"))  (Bool  "for" (Set (Var "G")) "being"    ($#m2_rcomp_3 :::"IntervalCoverPts"::: )   "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )) & (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "F")) "is"   ($#v1_rcomp_3 :::"connected"::: )  ) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s"))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "C"))))) "holds"  (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  "(" (Set (Var "C"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "G"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n"))))))))) ; 
 
theorem :: RCOMP_3:64 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )  (Bool  "for" (Set (Var "C")) "being"    ($#m1_rcomp_3 :::"IntervalCover"::: )   "of" (Set (Var "F"))  (Bool  "for" (Set (Var "G")) "being"    ($#m2_rcomp_3 :::"IntervalCoverPts"::: )   "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )) & (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "F")) "is"   ($#v1_rcomp_3 :::"connected"::: )  ) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s"))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "C"))))) "holds"  (Bool (Set (Set (Var "G"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  "(" (Set (Var "C"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )))))))) ; 
 
theorem :: RCOMP_3:65 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )  (Bool  "for" (Set (Var "C")) "being"    ($#m1_rcomp_3 :::"IntervalCover"::: )   "of" (Set (Var "F"))  (Bool  "for" (Set (Var "G")) "being"    ($#m2_rcomp_3 :::"IntervalCoverPts"::: )   "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )) & (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "F")) "is"   ($#v1_rcomp_3 :::"connected"::: )  ) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s")))) "holds"  (Bool (Set (Var "G")) "is"   ($#v5_valued_0 :::"increasing"::: )  ))))) ; 
 
theorem :: RCOMP_3:66 (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )  (Bool  "for" (Set (Var "C")) "being"    ($#m1_rcomp_3 :::"IntervalCover"::: )   "of" (Set (Var "F"))  (Bool  "for" (Set (Var "G")) "being"    ($#m2_rcomp_3 :::"IntervalCoverPts"::: )   "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )) & (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "F")) "is"   ($#v1_rcomp_3 :::"connected"::: )  ) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s"))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G"))))) "holds"  (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  "(" (Set (Var "G"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" ) "," (Set  "(" (Set (Var "G"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ($#k1_rcomp_1 :::".]"::: ) )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "C"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n"))))))))) ;