:: TOPREALB  semantic presentation begin  













registration
cluster (Set bbbadK4_XXREAL_1((Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1))) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 

cluster (Set bbbadK1_XXREAL_1((Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Num 1))) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 

cluster (Set bbbadK4_XXREAL_1((Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) "," (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ))) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; registration
cluster (Set   ($#k16_sin_cos :::"sin"::: )  ) ->   ($#v1_fcont_1 :::"continuous"::: )   ; 

cluster (Set   ($#k19_sin_cos :::"cos"::: )  ) ->   ($#v1_fcont_1 :::"continuous"::: )   ; 

cluster (Set   ($#k1_sin_cos6 :::"arcsin"::: )  ) ->   ($#v1_fcont_1 :::"continuous"::: )   ; 

cluster (Set   ($#k4_sin_cos6 :::"arccos"::: )  ) ->   ($#v1_fcont_1 :::"continuous"::: )   ; 
end; 
theorem :: TOPREALB:1 (Bool  "for" (Set (Var "a")) "," (Set (Var "r")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "r")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k1_fcont_1 :::"AffineMap"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "r"))))) ; 
 
theorem :: TOPREALB:2 (Bool  "for" (Set (Var "a")) "," (Set (Var "r")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "r")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k1_fcont_1 :::"AffineMap"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "r"))))) ; 
 registrationlet "a" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "b" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k1_fcont_1 :::"AffineMap"::: )   "(" "a" "," "b" ")" ) ->   ($#v2_funct_1 :::"one-to-one"::: )     ($#v2_funct_2 :::"onto"::: )   ; 
end; definitionlet "a", "b" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"IntIntervals":::  "(" "a" "," "b" ")"  ->    ($#m1_hidden :::"set"::: )   equals :: TOPREALB:def 1  "{"  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" "a"  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "n")) ")" ) "," (Set  "(" "b"  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "n")) ")" ) ($#k2_rcomp_1 :::".["::: ) ) where n "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  ) : (Bool verum)  "}"  ; end; 






:: deftheorem    defines :::"IntIntervals"::: TOPREALB:def 1 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k1_toprealb :::"IntIntervals"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "n")) ")" ) "," (Set  "(" (Set (Var "b"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "n")) ")" ) ($#k2_rcomp_1 :::".["::: ) ) where n "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  ) : (Bool verum)  "}"  )); 
 
theorem :: TOPREALB:3 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_toprealb :::"IntIntervals"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool  "ex" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_numbers :::"INT"::: )  ) "st" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "n")) ")" ) "," (Set  "(" (Set (Var "b"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "n")) ")" ) ($#k2_rcomp_1 :::".["::: ) )))  ")" ))) ; 
 registrationlet "a", "b" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k1_toprealb :::"IntIntervals"::: )   "(" "a" "," "b" ")" ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: TOPREALB:4 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "b"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<="::: )  (Num 1))) "holds"  (Bool (Set   ($#k1_toprealb :::"IntIntervals"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is"   ($#v4_taxonom2 :::"mutually-disjoint"::: )  )) ; 
 definitionlet "a", "b" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; :: original: :::"IntIntervals"::: redefine func  :::"IntIntervals":::  "(" "a" "," "b" ")"  ->   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  ($#k2_topalg_2 :::"R^1"::: ) ); end; definitionlet "a", "b" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; :: original: :::"IntIntervals"::: redefine func  :::"IntIntervals":::  "(" "a" "," "b" ")"  ->   ($#v1_tops_2 :::"open"::: )    ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  ($#k2_topalg_2 :::"R^1"::: ) ); end; begin  definitionlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"R^1"::: "r" ->   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k2_topalg_2 :::"R^1"::: ) ) equals :: TOPREALB:def 2 "r"; end; 





:: deftheorem    defines :::"R^1"::: TOPREALB:def 2 :  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_toprealb :::"R^1"::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set (Var "r")))); 
 definitionlet "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ); func  :::"R^1"::: "A" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_topalg_2 :::"R^1"::: ) ) equals :: TOPREALB:def 3 "A"; end; 





:: deftheorem    defines :::"R^1"::: TOPREALB:def 3 :  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k5_toprealb :::"R^1"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "A")))); 
 registrationlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ); 
cluster (Set   ($#k5_toprealb :::"R^1"::: )  "A") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; registrationlet "A" be   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ); 
cluster (Set   ($#k5_toprealb :::"R^1"::: )  "A") ->   ($#v3_pre_topc :::"open"::: )   ; 
end; registrationlet "A" be   ($#v2_rcomp_1 :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ); 
cluster (Set   ($#k5_toprealb :::"R^1"::: )  "A") ->   ($#v4_pre_topc :::"closed"::: )   ; 
end; registrationlet "A" be   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ); 
cluster (Set (Set  ($#k2_topalg_2 :::"R^1"::: ) )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k5_toprealb :::"R^1"::: )  "A" ")" )) ->   ($#v1_tsep_1 :::"open"::: )   ; 
end; registrationlet "A" be   ($#v2_rcomp_1 :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ); 
cluster (Set (Set  ($#k2_topalg_2 :::"R^1"::: ) )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k5_toprealb :::"R^1"::: )  "A" ")" )) ->   ($#v1_borsuk_1 :::"closed"::: )   ; 
end; definitionlet "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ); func  :::"R^1"::: "f" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  ($#k2_topalg_2 :::"R^1"::: ) )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k5_toprealb :::"R^1"::: )  (Set  "("  ($#k1_relset_1 :::"dom"::: )  "f" ")" ) ")" ) ")" ) "," (Set  "(" (Set  ($#k2_topalg_2 :::"R^1"::: ) )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k5_toprealb :::"R^1"::: )  (Set  "("  ($#k2_relset_1 :::"rng"::: )  "f" ")" ) ")" ) ")" ) equals :: TOPREALB:def 4 "f"; end; 





:: deftheorem    defines :::"R^1"::: TOPREALB:def 4 :  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k6_toprealb :::"R^1"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "f")))); 
 registrationlet "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ); 
cluster (Set   ($#k6_toprealb :::"R^1"::: )  "f") ->   ($#v2_funct_2 :::"onto"::: )   ; 
end; registrationlet "f" be   ($#v2_funct_1 :::"one-to-one"::: )    ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ); 
cluster (Set   ($#k6_toprealb :::"R^1"::: )  "f") ->   ($#v2_funct_1 :::"one-to-one"::: )   ; 
end; 
theorem :: TOPREALB:5 (Bool (Set (Set  ($#k2_topalg_2 :::"R^1"::: ) )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k5_toprealb :::"R^1"::: )  (Set  "("  ($#k2_subset_1 :::"[#]"::: )  (Set  ($#k1_numbers :::"REAL"::: ) ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_topalg_2 :::"R^1"::: )  )) ; 
 
theorem :: TOPREALB:6 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))) "holds"  (Bool (Set (Set  ($#k2_topalg_2 :::"R^1"::: ) )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k5_toprealb :::"R^1"::: )  (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_topalg_2 :::"R^1"::: )  ))) ; 
 
theorem :: TOPREALB:7 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set (Var "f")) "is"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_topalg_2 :::"R^1"::: ) ) "," (Set  "(" (Set  ($#k2_topalg_2 :::"R^1"::: ) )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k5_toprealb :::"R^1"::: )  (Set  "("  ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")) ")" ) ")" ) ")" ))) ; 
 
theorem :: TOPREALB:8 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set (Var "f")) "is"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_topalg_2 :::"R^1"::: ) ) "," (Set  ($#k2_topalg_2 :::"R^1"::: ) ))) ; 
 registrationlet "f" be   ($#v1_fcont_1 :::"continuous"::: )    ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ); 
cluster (Set   ($#k6_toprealb :::"R^1"::: )  "f") ->   ($#v5_pre_topc :::"continuous"::: )   ; 
end; registrationlet "a" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "b" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k6_toprealb :::"R^1"::: )  (Set  "("  ($#k1_fcont_1 :::"AffineMap"::: )   "(" "a" "," "b" ")"  ")" )) ->   ($#v1_t_0topsp :::"open"::: )   ; 
end; begin  definitionlet "S" be    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set   ($#k15_euclid :::"TOP-REAL"::: )  (Num 2)); attr "S" is  :::"being_simple_closed_curve":::  means :: TOPREALB:def 5 (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") "is"   ($#m1_subset_1 :::"Simple_closed_curve":::)); end; 




:: deftheorem    defines :::"being_simple_closed_curve"::: TOPREALB:def 5 :  (Bool  "for" (Set (Var "S")) "being"    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set   ($#k15_euclid :::"TOP-REAL"::: )  (Num 2)) "holds"   (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v1_toprealb :::"being_simple_closed_curve"::: )  ) "iff" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "is"   ($#m1_subset_1 :::"Simple_closed_curve":::))  ")" )); 
 registration
cluster   ($#v1_toprealb :::"being_simple_closed_curve"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_compts_1 :::"compact"::: )     ($#v1_borsuk_2 :::"pathwise_connected"::: )    for    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set   ($#k15_euclid :::"TOP-REAL"::: )  (Num 2)); 
end; registrationlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )  ; let "x" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); 
cluster (Set   ($#k3_topreal9 :::"Sphere"::: )   "(" "x" "," "r" ")" ) ->   ($#v1_topreal2 :::"being_simple_closed_curve"::: )   ; 
end; definitionlet "n" be   ($#m1_hidden :::"Nat":::); let "x" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); let "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"Tcircle":::  "(" "x" "," "r" ")"  ->    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set   ($#k15_euclid :::"TOP-REAL"::: )  "n") equals :: TOPREALB:def 6 (Set (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k3_topreal9 :::"Sphere"::: )   "(" "x" "," "r" ")"  ")" )); end; 







:: deftheorem    defines :::"Tcircle"::: TOPREALB:def 6 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k7_toprealb :::"Tcircle"::: )   "(" (Set (Var "x")) "," (Set (Var "r")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k3_topreal9 :::"Sphere"::: )   "(" (Set (Var "x")) "," (Set (Var "r")) ")"  ")" )))))); 
 registrationlet "n" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::); let "x" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); let "r" be   ($#v1_xreal_0 :::"real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k7_toprealb :::"Tcircle"::: )   "(" "x" "," "r" ")" ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_pre_topc :::"strict"::: )   ; 
end; 
theorem :: TOPREALB:9 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k7_toprealb :::"Tcircle"::: )   "(" (Set (Var "x")) "," (Set (Var "r")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_topreal9 :::"Sphere"::: )   "(" (Set (Var "x")) "," (Set (Var "r")) ")" ))))) ; 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); let "x" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); let "r" be   ($#v1_xboole_0 :::"empty"::: )     ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k7_toprealb :::"Tcircle"::: )   "(" "x" "," "r" ")" ) ->   ($#v7_struct_0 :::"trivial"::: )   ; 
end; 
theorem :: TOPREALB:10 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k7_toprealb :::"Tcircle"::: )   "(" (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) ")" ) "," (Set (Var "r")) ")" ) "is"    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set   ($#k1_topreala :::"Trectangle"::: )   "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set (Var "r")) "," (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set (Var "r")) ")" ))) ; 
 registrationlet "x" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); let "r" be   ($#v1_xreal_0 :::"real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k7_toprealb :::"Tcircle"::: )   "(" "x" "," "r" ")" ) ->   ($#v1_toprealb :::"being_simple_closed_curve"::: )   ; 
end; registration
cluster   ($#v1_pre_topc :::"strict"::: )     ($#v2_pre_topc :::"TopSpace-like"::: )   bbbadV1_MONOID_0() bbbadV2_MONOID_0()   ($#v1_toprealb :::"being_simple_closed_curve"::: )    for    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set   ($#k15_euclid :::"TOP-REAL"::: )  (Num 2)); 
end; 
theorem :: TOPREALB:11 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#v1_toprealb :::"being_simple_closed_curve"::: )     ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set   ($#k15_euclid :::"TOP-REAL"::: )  (Num 2)) "holds"  (Bool (Set (Var "S")) "," (Set (Var "T"))  ($#r2_borsuk_3 :::"are_homeomorphic"::: )  )) ; 
 definitionlet "n" be   ($#m1_hidden :::"Nat":::); func  :::"Tunit_circle"::: "n" ->    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set   ($#k15_euclid :::"TOP-REAL"::: )  "n") equals :: TOPREALB:def 7 (Set   ($#k7_toprealb :::"Tcircle"::: )   "(" (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ) ")" ) "," (Num 1) ")" ); end; 





:: deftheorem    defines :::"Tunit_circle"::: TOPREALB:def 7 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k8_toprealb :::"Tunit_circle"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k7_toprealb :::"Tcircle"::: )   "(" (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) ")" ) "," (Num 1) ")" ))); 
 registrationlet "n" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Nat":::); 
cluster (Set   ($#k8_toprealb :::"Tunit_circle"::: )  "n") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )  ; 
end; 
theorem :: TOPREALB:12 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Set (Var "n")) ")" ))) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "x")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Num 1)))) ; 
 
theorem :: TOPREALB:13 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" ))) "holds"  (Bool  "("  (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "x"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "x"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Num 1))  ")" )) ; 
 
theorem :: TOPREALB:14 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" )) & (Bool (Set (Set (Var "x"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "x"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: TOPREALB:15 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" )) & (Bool (Set (Set (Var "x"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1)))) "holds"  (Bool (Set (Set (Var "x"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: TOPREALB:16 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" )) & (Bool (Set (Set (Var "x"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "x"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: TOPREALB:17 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" )) & (Bool (Set (Set (Var "x"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1)))) "holds"  (Bool (Set (Set (Var "x"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: TOPREALB:18 (Bool (Set   ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2)) "is"    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set   ($#k1_topreala :::"Trectangle"::: )   "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Num 1) "," (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Num 1) ")" )) ; 
 
theorem :: TOPREALB:19 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k7_toprealb :::"Tcircle"::: )   "(" (Set (Var "x")) "," (Set (Var "r")) ")"  ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "r"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "b")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "x")))))  ")" )) "holds"  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ))))) ; 
 registration
cluster (Set   ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2)) ->   ($#v1_toprealb :::"being_simple_closed_curve"::: )   ; 
end; 
theorem :: TOPREALB:20 (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set   ($#k7_toprealb :::"Tcircle"::: )   "(" (Set (Var "x")) "," (Set (Var "r")) ")" ) "," (Set   ($#k7_toprealb :::"Tcircle"::: )   "(" (Set (Var "y")) "," (Set (Var "s")) ")" )  ($#r2_borsuk_3 :::"are_homeomorphic"::: )  )))) ; 
 registrationlet "x" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); let "r" be   ($#v1_xreal_0 :::"real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k7_toprealb :::"Tcircle"::: )   "(" "x" "," "r" ")" ) ->   ($#v1_borsuk_2 :::"pathwise_connected"::: )   ; 
end; definitionfunc  :::"c[10]":::  ->   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" ) equals :: TOPREALB:def 8 (Set  ($#k19_euclid :::"|["::: ) (Num 1) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ); func  :::"c[-10]":::  ->   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" ) equals :: TOPREALB:def 9 (Set  ($#k19_euclid :::"|["::: ) (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ); end; 








:: deftheorem    defines :::"c[10]"::: TOPREALB:def 8 :  (Bool (Set   ($#k9_toprealb :::"c[10]"::: )  )  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Num 1) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )); 
 
:: deftheorem    defines :::"c[-10]"::: TOPREALB:def 9 :  (Bool (Set   ($#k10_toprealb :::"c[-10]"::: )  )  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) )); 
 definitionlet "p" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" ); func  :::"Topen_unit_circle"::: "p" ->   ($#v1_pre_topc :::"strict"::: )     ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set   ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2)) means :: TOPREALB:def 10 (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" ))  ($#k6_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) "p" ($#k6_domain_1 :::"}"::: ) ))); end; 





:: deftheorem    defines :::"Topen_unit_circle"::: TOPREALB:def 10 :  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "b2")) "being"   ($#v1_pre_topc :::"strict"::: )     ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set   ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2)) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_toprealb :::"Topen_unit_circle"::: )  (Set (Var "p")))) "iff" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" ))  ($#k6_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )))  ")" ))); 
 registrationlet "p" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" ); 
cluster (Set   ($#k11_toprealb :::"Topen_unit_circle"::: )  "p") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_pre_topc :::"strict"::: )   ; 
end; 
theorem :: TOPREALB:21 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" )  "holds" (Bool (Set (Var "p")) "is" (Bool  "not"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k11_toprealb :::"Topen_unit_circle"::: )  (Set (Var "p")) ")" )))) ; 
 
theorem :: TOPREALB:22 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k11_toprealb :::"Topen_unit_circle"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set  "(" (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" ) ")" )  ($#k7_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ) ")" )))) ; 
 
theorem :: TOPREALB:23 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Set (Var "q")))) "holds"  (Bool (Set (Var "q")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k11_toprealb :::"Topen_unit_circle"::: )  (Set (Var "p")) ")" ))) ; 
 
theorem :: TOPREALB:24 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k11_toprealb :::"Topen_unit_circle"::: )  (Set  ($#k9_toprealb :::"c[10]"::: ) ) ")" )) & (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_toprealb :::"c[-10]"::: )  ))) ; 
 
theorem :: TOPREALB:25 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k11_toprealb :::"Topen_unit_circle"::: )  (Set  ($#k10_toprealb :::"c[-10]"::: ) ) ")" )) & (Bool (Set (Set (Var "p"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_toprealb :::"c[10]"::: )  ))) ; 
 
theorem :: TOPREALB:26 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k11_toprealb :::"Topen_unit_circle"::: )  (Set (Var "p")) ")" ))) "holds"  (Bool  "("  (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "x"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "x"))  ($#k18_euclid :::"`2"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Num 1))  ")" ))) ; 
 
theorem :: TOPREALB:27 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k11_toprealb :::"Topen_unit_circle"::: )  (Set  ($#k9_toprealb :::"c[10]"::: ) ) ")" ))) "holds"  (Bool  "("  (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "x"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Num 1))  ")" )) ; 
 
theorem :: TOPREALB:28 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k11_toprealb :::"Topen_unit_circle"::: )  (Set  ($#k10_toprealb :::"c[-10]"::: ) ) ")" ))) "holds"  (Bool  "("  (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "x"))  ($#k17_euclid :::"`1"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Num 1))  ")" )) ; 
 registrationlet "p" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" ); 
cluster (Set   ($#k11_toprealb :::"Topen_unit_circle"::: )  "p") ->   ($#v1_pre_topc :::"strict"::: )     ($#v1_tsep_1 :::"open"::: )   ; 
end; 
theorem :: TOPREALB:29 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k11_toprealb :::"Topen_unit_circle"::: )  (Set (Var "p"))) "," (Set   ($#k1_borsuk_4 :::"I(01)"::: )  )  ($#r1_borsuk_3 :::"are_homeomorphic"::: )  )) ; 
 
theorem :: TOPREALB:30 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" ) "holds"  (Bool (Set   ($#k11_toprealb :::"Topen_unit_circle"::: )  (Set (Var "p"))) "," (Set   ($#k11_toprealb :::"Topen_unit_circle"::: )  (Set (Var "q")))  ($#r2_borsuk_3 :::"are_homeomorphic"::: )  )) ; 
 begin  definitionfunc  :::"CircleMap":::  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_topalg_2 :::"R^1"::: ) ) "," (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" ) means :: TOPREALB:def 11 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" ) "," (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" ) ($#k19_euclid :::"]|"::: ) ))); end; 




:: deftheorem    defines :::"CircleMap"::: TOPREALB:def 11 :  (Bool  "for" (Set (Var "b1")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_topalg_2 :::"R^1"::: ) ) "," (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k12_toprealb :::"CircleMap"::: )  )) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "b1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "("  ($#k21_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" ) "," (Set  "("  ($#k18_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" ) ")" ) ($#k19_euclid :::"]|"::: ) )))  ")" )); 
 
theorem :: TOPREALB:31 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  ($#k12_toprealb :::"CircleMap"::: ) )  ($#k1_funct_1 :::"."::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k12_toprealb :::"CircleMap"::: ) )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "r"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "i")) ")" ))))) ; 
 
theorem :: TOPREALB:32 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set (Set  ($#k12_toprealb :::"CircleMap"::: ) )  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_toprealb :::"c[10]"::: )  ))) ; 
 
theorem :: TOPREALB:33 (Bool (Set (Set  ($#k12_toprealb :::"CircleMap"::: ) )  ($#k8_relset_1 :::"""::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  ($#k9_toprealb :::"c[10]"::: ) ) ($#k6_domain_1 :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_numbers :::"INT"::: )  )) ; 
 
theorem :: TOPREALB:34 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k4_int_1 :::"frac"::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2)))) "holds"  (Bool (Set (Set  ($#k12_toprealb :::"CircleMap"::: ) )  ($#k1_funct_1 :::"."::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) "," (Set  ($#k6_numbers :::"0"::: ) ) ($#k19_euclid :::"]|"::: ) ))) ; 
 
theorem :: TOPREALB:35 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k4_int_1 :::"frac"::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 4)))) "holds"  (Bool (Set (Set  ($#k12_toprealb :::"CircleMap"::: ) )  ($#k1_funct_1 :::"."::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k19_euclid :::"]|"::: ) ))) ; 
 
theorem :: TOPREALB:36 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k4_int_1 :::"frac"::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 4)))) "holds"  (Bool (Set (Set  ($#k12_toprealb :::"CircleMap"::: ) )  ($#k1_funct_1 :::"."::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ) ($#k19_euclid :::"]|"::: ) ))) ; 
 
theorem :: TOPREALB:37 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set (Set  ($#k12_toprealb :::"CircleMap"::: ) )  ($#k1_funct_1 :::"."::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set  "(" (Set  "(" (Set  ($#k19_sin_cos :::"cos"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k1_fcont_1 :::"AffineMap"::: )   "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) "," (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "i")) ")" ) ")"  ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Set  "(" (Set  ($#k16_sin_cos :::"sin"::: ) )  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k1_fcont_1 :::"AffineMap"::: )   "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) "," (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "j")) ")" ) ")"  ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "r")) ")" ) ($#k19_euclid :::"]|"::: ) )))) ; 
 registration
cluster (Set   ($#k12_toprealb :::"CircleMap"::: )  ) ->   ($#v5_pre_topc :::"continuous"::: )   ; 
end; 
theorem :: TOPREALB:38 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_topalg_2 :::"R^1"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  ($#k2_topalg_2 :::"R^1"::: ) )  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" ) "," (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set  ($#k3_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k3_rcomp_1 :::".["::: ) )  ($#r1_tarski :::"c="::: )  (Set (Var "A"))) & (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k12_toprealb :::"CircleMap"::: ) )  ($#k2_partfun1 :::"|"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Var "f")) "is"   ($#v2_funct_2 :::"onto"::: )  ))) ; 
 registration
cluster (Set   ($#k12_toprealb :::"CircleMap"::: )  ) ->   ($#v2_funct_2 :::"onto"::: )   ; 
end; registrationlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set bbbadK5_RELAT_1((Set  ($#k12_toprealb :::"CircleMap"::: ) ) "," (Set  ($#k3_rcomp_1 :::"[."::: ) "r" "," (Set  "(" "r"  ($#k3_real_1 :::"+"::: )  (Num 1) ")" ) ($#k3_rcomp_1 :::".["::: ) ))) ->   ($#v2_funct_1 :::"one-to-one"::: )   ; 
end; registrationlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set bbbadK5_RELAT_1((Set  ($#k12_toprealb :::"CircleMap"::: ) ) "," (Set  ($#k2_rcomp_1 :::"]."::: ) "r" "," (Set  "(" "r"  ($#k3_real_1 :::"+"::: )  (Num 1) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) ->   ($#v2_funct_1 :::"one-to-one"::: )   ; 
end; 
theorem :: TOPREALB:39 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "b"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<="::: )  (Num 1))) "holds"  (Bool  "for" (Set (Var "d")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_toprealb :::"IntIntervals"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) "holds"  (Bool (Set (Set  ($#k12_toprealb :::"CircleMap"::: ) )  ($#k2_partfun1 :::"|"::: )  (Set (Var "d"))) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ))) ; 
 
theorem :: TOPREALB:40 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "d")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_toprealb :::"IntIntervals"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) "holds"  (Bool (Set (Set  ($#k12_toprealb :::"CircleMap"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k12_toprealb :::"CircleMap"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k5_setfam_1 :::"union"::: )  (Set  "("  ($#k3_toprealb :::"IntIntervals"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) ")" ))))) ; 
 definitionlet "r" be   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k2_topalg_2 :::"R^1"::: ) ); func  :::"CircleMap"::: "r" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  ($#k2_topalg_2 :::"R^1"::: ) )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k5_toprealb :::"R^1"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) "r" "," (Set  "(" "r"  ($#k3_real_1 :::"+"::: )  (Num 1) ")" ) ($#k2_rcomp_1 :::".["::: ) ) ")" ) ")" ) "," (Set  "("  ($#k11_toprealb :::"Topen_unit_circle"::: )  (Set  "(" (Set  ($#k12_toprealb :::"CircleMap"::: ) )  ($#k3_funct_2 :::"."::: )  "r" ")" ) ")" ) equals :: TOPREALB:def 12 (Set (Set  ($#k12_toprealb :::"CircleMap"::: ) )  ($#k2_partfun1 :::"|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) "r" "," (Set  "(" "r"  ($#k3_real_1 :::"+"::: )  (Num 1) ")" ) ($#k2_rcomp_1 :::".["::: ) )); end; 





:: deftheorem    defines :::"CircleMap"::: TOPREALB:def 12 :  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k2_topalg_2 :::"R^1"::: ) ) "holds"  (Bool (Set   ($#k13_toprealb :::"CircleMap"::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k12_toprealb :::"CircleMap"::: ) )  ($#k2_partfun1 :::"|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "r")) "," (Set  "(" (Set (Var "r"))  ($#k3_real_1 :::"+"::: )  (Num 1) ")" ) ($#k2_rcomp_1 :::".["::: ) )))); 
 
theorem :: TOPREALB:41 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k13_toprealb :::"CircleMap"::: )  (Set  "("  ($#k4_toprealb :::"R^1"::: )  (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "i")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k13_toprealb :::"CircleMap"::: )  (Set  "("  ($#k4_toprealb :::"R^1"::: )  (Set (Var "a")) ")" ) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set  "("  ($#k1_fcont_1 :::"AffineMap"::: )   "(" (Num 1) "," (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "i")) ")" ) ")"  ")" )  ($#k2_partfun1 :::"|"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "i")) ")" ) "," (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "i")) ")" )  ($#k3_real_1 :::"+"::: )  (Num 1) ")" ) ($#k2_rcomp_1 :::".["::: ) ) ")" ))))) ; 
 registrationlet "r" be   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k2_topalg_2 :::"R^1"::: ) ); 
cluster (Set   ($#k13_toprealb :::"CircleMap"::: )  "r") ->   ($#v2_funct_1 :::"one-to-one"::: )     ($#v2_funct_2 :::"onto"::: )     ($#v5_pre_topc :::"continuous"::: )   ; 
end; definitionfunc  :::"Circle2IntervalR":::  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k11_toprealb :::"Topen_unit_circle"::: )  (Set  ($#k9_toprealb :::"c[10]"::: ) ) ")" ) "," (Set  "(" (Set  ($#k2_topalg_2 :::"R^1"::: ) )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k5_toprealb :::"R^1"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ) ")" ) ")" ) means :: TOPREALB:def 13 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k11_toprealb :::"Topen_unit_circle"::: )  (Set  ($#k9_toprealb :::"c[10]"::: ) ) ")" ) (Bool  "ex" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) )) &  "("  (Bool (Bool (Set (Var "y"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_sin_cos6 :::"arccos"::: )  (Set (Var "x")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" )))  ")"  &  "("  (Bool (Bool (Set (Var "y"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k6_sin_cos6 :::"arccos"::: )  (Set (Var "x")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" )))  ")"   ")" ))); end; 




:: deftheorem    defines :::"Circle2IntervalR"::: TOPREALB:def 13 :  (Bool  "for" (Set (Var "b1")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k11_toprealb :::"Topen_unit_circle"::: )  (Set  ($#k9_toprealb :::"c[10]"::: ) ) ")" ) "," (Set  "(" (Set  ($#k2_topalg_2 :::"R^1"::: ) )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k5_toprealb :::"R^1"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ) ")" ) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k14_toprealb :::"Circle2IntervalR"::: )  )) "iff" (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k11_toprealb :::"Topen_unit_circle"::: )  (Set  ($#k9_toprealb :::"c[10]"::: ) ) ")" ) (Bool  "ex" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) )) &  "("  (Bool (Bool (Set (Var "y"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set (Set (Var "b1"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_sin_cos6 :::"arccos"::: )  (Set (Var "x")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" )))  ")"  &  "("  (Bool (Bool (Set (Var "y"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set (Set (Var "b1"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k6_sin_cos6 :::"arccos"::: )  (Set (Var "x")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" )))  ")"   ")" )))  ")" )); 
 definitionfunc  :::"Circle2IntervalL":::  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k11_toprealb :::"Topen_unit_circle"::: )  (Set  ($#k10_toprealb :::"c[-10]"::: ) ) ")" ) "," (Set  "(" (Set  ($#k2_topalg_2 :::"R^1"::: ) )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k5_toprealb :::"R^1"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) "," (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) ) ")" ) ")" ) means :: TOPREALB:def 14 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k11_toprealb :::"Topen_unit_circle"::: )  (Set  ($#k10_toprealb :::"c[-10]"::: ) ) ")" ) (Bool  "ex" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) )) &  "("  (Bool (Bool (Set (Var "y"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k6_sin_cos6 :::"arccos"::: )  (Set (Var "x")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" )))  ")"  &  "("  (Bool (Bool (Set (Var "y"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k6_sin_cos6 :::"arccos"::: )  (Set (Var "x")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" )))  ")"   ")" ))); end; 




:: deftheorem    defines :::"Circle2IntervalL"::: TOPREALB:def 14 :  (Bool  "for" (Set (Var "b1")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k11_toprealb :::"Topen_unit_circle"::: )  (Set  ($#k10_toprealb :::"c[-10]"::: ) ) ")" ) "," (Set  "(" (Set  ($#k2_topalg_2 :::"R^1"::: ) )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k5_toprealb :::"R^1"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) "," (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) ) ")" ) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k15_toprealb :::"Circle2IntervalL"::: )  )) "iff" (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k11_toprealb :::"Topen_unit_circle"::: )  (Set  ($#k10_toprealb :::"c[-10]"::: ) ) ")" ) (Bool  "ex" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set  ($#k19_euclid :::"|["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k19_euclid :::"]|"::: ) )) &  "("  (Bool (Bool (Set (Var "y"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set (Set (Var "b1"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k6_sin_cos6 :::"arccos"::: )  (Set (Var "x")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" )))  ")"  &  "("  (Bool (Bool (Set (Var "y"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set (Set (Var "b1"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k6_sin_cos6 :::"arccos"::: )  (Set (Var "x")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" )))  ")"   ")" )))  ")" )); 
 
theorem :: TOPREALB:42 (Bool (Set (Set  "("  ($#k13_toprealb :::"CircleMap"::: )  (Set  "("  ($#k4_toprealb :::"R^1"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")" )  ($#k2_tops_2 :::"""::: )  )  ($#r1_funct_2 :::"="::: )  (Set   ($#k14_toprealb :::"Circle2IntervalR"::: )  )) ; 
 
theorem :: TOPREALB:43 (Bool (Set (Set  "("  ($#k13_toprealb :::"CircleMap"::: )  (Set  "("  ($#k4_toprealb :::"R^1"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k2_tops_2 :::"""::: )  )  ($#r1_funct_2 :::"="::: )  (Set   ($#k15_toprealb :::"Circle2IntervalL"::: )  )) ; 
 registration
cluster (Set   ($#k14_toprealb :::"Circle2IntervalR"::: )  ) ->   ($#v2_funct_1 :::"one-to-one"::: )     ($#v2_funct_2 :::"onto"::: )     ($#v5_pre_topc :::"continuous"::: )   ; 

cluster (Set   ($#k15_toprealb :::"Circle2IntervalL"::: )  ) ->   ($#v2_funct_1 :::"one-to-one"::: )     ($#v2_funct_2 :::"onto"::: )     ($#v5_pre_topc :::"continuous"::: )   ; 
end; registrationlet "i" be   ($#m1_hidden :::"Integer":::); 
cluster (Set   ($#k13_toprealb :::"CircleMap"::: )  (Set  "("  ($#k4_toprealb :::"R^1"::: )  "i" ")" )) ->   ($#v1_t_0topsp :::"open"::: )   ; 

cluster (Set   ($#k13_toprealb :::"CircleMap"::: )  (Set  "("  ($#k4_toprealb :::"R^1"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" )  ($#k7_real_1 :::"+"::: )  "i" ")" ) ")" )) ->   ($#v1_t_0topsp :::"open"::: )   ; 
end; registration
cluster (Set   ($#k14_toprealb :::"Circle2IntervalR"::: )  ) ->   ($#v1_t_0topsp :::"open"::: )   ; 

cluster (Set   ($#k15_toprealb :::"Circle2IntervalL"::: )  ) ->   ($#v1_t_0topsp :::"open"::: )   ; 
end; 
theorem :: TOPREALB:44 (Bool (Set   ($#k13_toprealb :::"CircleMap"::: )  (Set  "("  ($#k4_toprealb :::"R^1"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" )) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) ; 
 
theorem :: TOPREALB:45 (Bool  "ex" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "F"))  ($#r1_hidden :::"="::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set  "(" (Set  ($#k12_toprealb :::"CircleMap"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ) ")" ) "," (Set  "(" (Set  ($#k12_toprealb :::"CircleMap"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) "," (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) ) ")" ) ($#k7_domain_1 :::"}"::: ) )) & (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" )) & (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool  "("   "for" (Set (Var "U")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" ) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "U"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k12_toprealb :::"CircleMap"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) )))) "implies" (Bool  "("  (Bool (Set   ($#k5_setfam_1 :::"union"::: )  (Set  "("  ($#k3_toprealb :::"IntIntervals"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k12_toprealb :::"CircleMap"::: ) )  ($#k8_relset_1 :::"""::: )  (Set (Var "U")))) & (Bool  "("   "for" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_topalg_2 :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_toprealb :::"IntIntervals"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ))) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  ($#k2_topalg_2 :::"R^1"::: ) )  ($#k1_pre_topc :::"|"::: )  (Set (Var "d")) ")" ) "," (Set  "(" (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "U")) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k12_toprealb :::"CircleMap"::: ) )  ($#k2_partfun1 :::"|"::: )  (Set (Var "d"))))) "holds"  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ))  ")" )  ")" )  ")"  &  "("  (Bool (Bool (Set (Var "U"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k12_toprealb :::"CircleMap"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set  ($#k2_rcomp_1 :::"]."::: ) (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) "," (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) )))) "implies" (Bool  "("  (Bool (Set   ($#k5_setfam_1 :::"union"::: )  (Set  "("  ($#k3_toprealb :::"IntIntervals"::: )   "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) "," (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k12_toprealb :::"CircleMap"::: ) )  ($#k8_relset_1 :::"""::: )  (Set (Var "U")))) & (Bool  "("   "for" (Set (Var "d")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_topalg_2 :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_toprealb :::"IntIntervals"::: )   "(" (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) "," (Set  "(" (Num 3)  ($#k10_real_1 :::"/"::: )  (Num 2) ")" ) ")" ))) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  ($#k2_topalg_2 :::"R^1"::: ) )  ($#k1_pre_topc :::"|"::: )  (Set (Var "d")) ")" ) "," (Set  "(" (Set  "("  ($#k8_toprealb :::"Tunit_circle"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "U")) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k12_toprealb :::"CircleMap"::: ) )  ($#k2_partfun1 :::"|"::: )  (Set (Var "d"))))) "holds"  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ))  ")" )  ")" )  ")"   ")" )  ")" )  ")" )) ;