:: TOPREALA  semantic presentation begin  








registrationlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "s" be   ($#v1_xreal_0 :::"real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set bbbadK4_XXREAL_1("r" "," (Set  "(" "r"  ($#k2_xcmplx_0 :::"+"::: )  "s" ")" ))) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 

cluster (Set bbbadK2_XXREAL_1("r" "," (Set  "(" "r"  ($#k2_xcmplx_0 :::"+"::: )  "s" ")" ))) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 

cluster (Set bbbadK3_XXREAL_1("r" "," (Set  "(" "r"  ($#k2_xcmplx_0 :::"+"::: )  "s" ")" ))) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 

cluster (Set bbbadK1_XXREAL_1("r" "," (Set  "(" "r"  ($#k2_xcmplx_0 :::"+"::: )  "s" ")" ))) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 

cluster (Set bbbadK4_XXREAL_1((Set  "(" "r"  ($#k6_xcmplx_0 :::"-"::: )  "s" ")" ) "," "r")) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 

cluster (Set bbbadK2_XXREAL_1((Set  "(" "r"  ($#k6_xcmplx_0 :::"-"::: )  "s" ")" ) "," "r")) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 

cluster (Set bbbadK3_XXREAL_1((Set  "(" "r"  ($#k6_xcmplx_0 :::"-"::: )  "s" ")" ) "," "r")) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 

cluster (Set bbbadK1_XXREAL_1((Set  "(" "r"  ($#k6_xcmplx_0 :::"-"::: )  "s" ")" ) "," "r")) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; registrationlet "r" be   ($#v1_xreal_0 :::"real"::: )    ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )    ($#m1_hidden :::"number"::: )  ; let "s" be   ($#v1_xreal_0 :::"real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set bbbadK4_XXREAL_1("r" "," "s")) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 

cluster (Set bbbadK2_XXREAL_1("r" "," "s")) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 

cluster (Set bbbadK3_XXREAL_1("r" "," "s")) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 

cluster (Set bbbadK1_XXREAL_1("r" "," "s")) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; registrationlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#v3_xxreal_0 :::"negative"::: )     ($#m1_hidden :::"number"::: )  ; let "s" be   ($#v1_xreal_0 :::"real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set bbbadK4_XXREAL_1("r" "," "s")) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 

cluster (Set bbbadK2_XXREAL_1("r" "," "s")) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 

cluster (Set bbbadK3_XXREAL_1("r" "," "s")) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 

cluster (Set bbbadK1_XXREAL_1("r" "," "s")) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; begin  
theorem :: TOPREALA:1 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "f"))  ($#k7_relat_1 :::".:"::: )  (Set (Var "X")))) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))) ; 
 
theorem :: TOPREALA:2 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"FinSequence":::)  (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Set (Var "i"))  ($#k3_real_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) "or" (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) "or" (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))) ; 
 
theorem :: TOPREALA:3 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y"))) & (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_card_3 :::"product"::: )  (Set  "("  "(" (Set (Var "x")) "," (Set (Var "y")) ")"   ($#k4_funct_4 :::"-->"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y")))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))  ")" ))) ; 
 
theorem :: TOPREALA:4 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set  ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) )  ($#r1_hidden :::"="::: )  (Set  "(" (Num 1) "," (Num 2) ")"   ($#k4_funct_4 :::"-->"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) ; 
 begin  registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_pre_topc :::"strict"::: )     ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v2_monoid_0 :::"constituted-FinSeqs"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; registrationlet "T" be   ($#v2_monoid_0 :::"constituted-FinSeqs"::: )    ($#l1_pre_topc :::"TopSpace":::); 
cluster   ->   ($#v2_monoid_0 :::"constituted-FinSeqs"::: )    for    ($#m1_pre_topc :::"SubSpace"::: )   "of" "T"; 
end; 
theorem :: TOPREALA:5 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Z")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "T"))  (Bool  "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "z")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Z"))  (Bool  "for" (Set (Var "N")) "being"   ($#v3_pre_topc :::"open"::: )     ($#m1_connsp_2 :::"a_neighborhood"::: )   "of" (Set (Var "t"))  (Bool  "for" (Set (Var "M")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Z"))  "st" (Bool (Bool (Set (Var "t"))  ($#r1_hidden :::"="::: )  (Set (Var "z"))) & (Bool (Set (Var "M"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "N"))  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "Z")) ")" )))) "holds"  (Bool (Set (Var "M")) "is"   ($#v3_pre_topc :::"open"::: )     ($#m1_connsp_2 :::"a_neighborhood"::: )   "of" (Set (Var "z"))))))))) ; 
 registration
cluster   ($#v2_struct_0 :::"empty"::: )     ($#v2_pre_topc :::"TopSpace-like"::: )    ->   ($#v1_tdlat_3 :::"discrete"::: )     ($#v2_tdlat_3 :::"anti-discrete"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; registrationlet "X" be   ($#v1_tdlat_3 :::"discrete"::: )    ($#l1_pre_topc :::"TopSpace":::); let "Y" be   ($#l1_pre_topc :::"TopSpace":::); 
cluster   ($#v1_funct_1 :::"Function-like"::: )     ($#v1_funct_2 :::"quasi_total"::: )    ->   ($#v5_pre_topc :::"continuous"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "Y") ($#k2_zfmisc_1 :::":]"::: ) )); 
end; 
theorem :: TOPREALA:6 (Bool  "for" (Set (Var "X")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Y")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  )))) ; 
 registrationlet "X" be   ($#l1_pre_topc :::"TopSpace":::); let "Y" be    ($#l1_pre_topc :::"TopStruct"::: )  ; 
cluster   ($#v1_funct_1 :::"Function-like"::: )     ($#v1_xboole_0 :::"empty"::: )     ($#v1_funct_2 :::"quasi_total"::: )    ->   ($#v5_pre_topc :::"continuous"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "Y") ($#k2_zfmisc_1 :::":]"::: ) )); 
end; 
theorem :: TOPREALA:7 (Bool  "for" (Set (Var "X")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "Z")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "Y"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Z")) "holds"  (Bool (Set (Var "f")) "is"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))))))) ; 
 
theorem :: TOPREALA:8 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set (Var "S"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "X")) ")" ) "," (Set  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "Y")) ")" )  "st" (Bool (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  )))))) ; 
 
theorem :: TOPREALA:9 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Z")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "T"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "Z"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_funct_2 :::"="::: )  (Set (Var "g"))) & (Bool (Set (Var "f")) "is"   ($#v1_t_0topsp :::"open"::: )  )) "holds"  (Bool (Set (Var "g")) "is"   ($#v1_t_0topsp :::"open"::: )  ))))) ; 
 
theorem :: TOPREALA:10 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "S1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "T1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set (Var "S"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "S1")) ")" ) "," (Set  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "T1")) ")" )  "st" (Bool (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "S1")))) & (Bool (Set (Var "g")) "is"   ($#v2_funct_2 :::"onto"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v1_t_0topsp :::"open"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )) "holds"  (Bool (Set (Var "g")) "is"   ($#v1_t_0topsp :::"open"::: )  )))))) ; 
 
theorem :: TOPREALA:11 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v1_t_0topsp :::"open"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v1_t_0topsp :::"open"::: )  )) "holds"  (Bool (Set (Set (Var "g"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "f"))) "is"   ($#v1_t_0topsp :::"open"::: )  )))) ; 
 
theorem :: TOPREALA:12 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#v1_tsep_1 :::"open"::: )     ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "Y"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Z"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "g"))) & (Bool (Set (Var "g")) "is"   ($#v1_t_0topsp :::"open"::: )  )) "holds"  (Bool (Set (Var "f")) "is"   ($#v1_t_0topsp :::"open"::: )  ))))) ; 
 
theorem :: TOPREALA:13 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_funct_2 :::"onto"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) "iff" (Bool (Set (Set (Var "f"))  ($#k2_tops_2 :::"""::: )  ) "is"   ($#v1_t_0topsp :::"open"::: )  )  ")" ))) ; 
 
theorem :: TOPREALA:14 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_funct_2 :::"onto"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v1_t_0topsp :::"open"::: )  ) "iff" (Bool (Set (Set (Var "f"))  ($#k2_tops_2 :::"""::: )  ) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" ))) ; 
 
theorem :: TOPREALA:15 (Bool  "for" (Set (Var "S")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "S")) "," (Set (Var "T"))  ($#r1_t_0topsp :::"are_homeomorphic"::: )  ) "iff" (Bool (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "S"))) "#)" ) "," (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T"))) "#)" )  ($#r1_t_0topsp :::"are_homeomorphic"::: )  )  ")" ))) ; 
 
theorem :: TOPREALA:16 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_funct_2 :::"onto"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v1_t_0topsp :::"open"::: )  )) "holds"  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ))) ; 
 begin  
theorem :: TOPREALA:17 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k1_numbers :::"REAL"::: ) )  ($#k7_funcop_1 :::"-->"::: )  (Set (Var "r"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k1_numbers :::"REAL"::: ) )) "is"   ($#v1_fcont_1 :::"continuous"::: )  ))) ; 
 
theorem :: TOPREALA:18 (Bool  "for" (Set (Var "f")) "," (Set (Var "f1")) "," (Set (Var "f2")) "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 (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set (Var "f1")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set (Var "f2")) ")" ))) & (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f1"))) "is"   ($#v3_rcomp_1 :::"open"::: )  ) & (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f2"))) "is"   ($#v3_rcomp_1 :::"open"::: )  ) & (Bool (Set (Set (Var "f1"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set (Var "f1")) ")" )) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool (Set (Set (Var "f2"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set (Var "f2")) ")" )) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool  "("   "for" (Set (Var "z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f1"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "z"))))  ")" ) & (Bool  "("   "for" (Set (Var "z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f2"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "z"))))  ")" )) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")) ")" )) "is"   ($#v1_fcont_1 :::"continuous"::: )  )) ; 
 
theorem :: TOPREALA:19 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k3_topmetr :::"R^1"::: ) )  (Bool  "for" (Set (Var "N")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "M")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_topmetr :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "M"))  ($#r1_hidden :::"="::: )  (Set (Var "N"))) & (Bool (Set (Var "N")) "is"    ($#m1_rcomp_1 :::"Neighbourhood"::: )   "of" (Set (Var "x")))) "holds"  (Bool (Set (Var "M")) "is"    ($#m1_connsp_2 :::"a_neighborhood"::: )   "of" (Set (Var "x")))))) ; 
 
theorem :: TOPREALA:20 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k3_topmetr :::"R^1"::: ) )  (Bool  "for" (Set (Var "M")) "being"    ($#m1_connsp_2 :::"a_neighborhood"::: )   "of" (Set (Var "x")) (Bool  "ex" (Set (Var "N")) "being"    ($#m1_rcomp_1 :::"Neighbourhood"::: )   "of" (Set (Var "x")) "st" (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set (Var "M")))))) ; 
 
theorem :: TOPREALA:21 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_topmetr :::"R^1"::: ) ) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k3_topmetr :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "g"))) & (Bool (Set (Var "g"))  ($#r1_fcont_1 :::"is_continuous_in"::: )  (Set (Var "x")))) "holds"  (Bool (Set (Var "f"))  ($#r1_tmap_1 :::"is_continuous_at"::: )  (Set (Var "x")))))) ; 
 
theorem :: TOPREALA:22 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_topmetr :::"R^1"::: ) ) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_funct_2 :::"="::: )  (Set (Var "g"))) & (Bool (Set (Var "g")) "is"   ($#v1_fcont_1 :::"continuous"::: )  )) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ))) ; 
 
theorem :: TOPREALA:23 (Bool  "for" (Set (Var "a")) "," (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r"))) & (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "holds"  (Bool (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k1_rcomp_1 :::".]"::: ) ) "is"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ))) ; 
 
theorem :: TOPREALA:24 (Bool  "for" (Set (Var "a")) "," (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r"))) & (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "holds"  (Bool (Set  ($#k2_rcomp_1 :::"]."::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k2_rcomp_1 :::".["::: ) ) "is"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ))) ; 
 
theorem :: TOPREALA:25 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))) "holds"  (Bool (Set  ($#k4_rcomp_1 :::"]."::: ) (Set (Var "r")) "," (Set (Var "b")) ($#k4_rcomp_1 :::".]"::: ) ) "is"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ))) ; 
 
theorem :: TOPREALA:26 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "holds"  (Bool (Set  ($#k3_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "r")) ($#k3_rcomp_1 :::".["::: ) ) "is"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ))) ; 
 
theorem :: TOPREALA:27 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))) "holds"  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" ) ($#k2_borsuk_1 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ) "," (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k1_rcomp_1 :::".]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) ; 
 begin  
theorem :: TOPREALA:28 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) )  ($#r1_hidden :::"="::: )  (Set  "(" (Num 1) "," (Num 2) ")"   ($#k4_funct_4 :::"-->"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) ; 
 
theorem :: TOPREALA:29 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Set  ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) )  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set  ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k19_euclid :::"]|"::: ) )  ($#k1_funct_1 :::"."::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" )) ; 
 
theorem :: TOPREALA:30 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k2_jgraph_6 :::"closed_inside_of_rectangle"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "," (Set (Var "s")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_card_3 :::"product"::: )  (Set  "("  "(" (Num 1) "," (Num 2) ")"   ($#k4_funct_4 :::"-->"::: )   "(" (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ) "," (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k1_rcomp_1 :::".]"::: ) ) ")"  ")" )))) ; 
 
theorem :: TOPREALA:31 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))) "holds"  (Bool (Set  ($#k19_euclid :::"|["::: ) (Set (Var "a")) "," (Set (Var "r")) ($#k19_euclid :::"]|"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_jgraph_6 :::"closed_inside_of_rectangle"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "," (Set (Var "s")) ")" ))) ; 
 definitionlet "a", "b", "c", "d" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"Trectangle":::  "(" "a" "," "b" "," "c" "," "d" ")"  ->    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set   ($#k15_euclid :::"TOP-REAL"::: )  (Num 2)) equals :: TOPREALA:def 1 (Set (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k2_jgraph_6 :::"closed_inside_of_rectangle"::: )   "(" "a" "," "b" "," "c" "," "d" ")"  ")" )); end; 








:: deftheorem    defines :::"Trectangle"::: TOPREALA:def 1 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k1_topreala :::"Trectangle"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k2_jgraph_6 :::"closed_inside_of_rectangle"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")"  ")" )))); 
 
theorem :: TOPREALA:32 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))) "holds"  (Bool  "not" (Bool (Set   ($#k1_topreala :::"Trectangle"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "," (Set (Var "s")) ")" ) "is"   ($#v2_struct_0 :::"empty"::: )  ))) ; 
 registrationlet "a", "c" be   ($#v1_xreal_0 :::"real"::: )    ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )    ($#m1_hidden :::"number"::: )  ; let "b", "d" be   ($#v1_xreal_0 :::"real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k1_topreala :::"Trectangle"::: )   "(" "a" "," "b" "," "c" "," "d" ")" ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )  ; 
end; definitionfunc  :::"R2Homeomorphism":::  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set  ($#k3_topmetr :::"R^1"::: ) ) "," (Set  ($#k3_topmetr :::"R^1"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) means :: TOPREALA:def 2 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ))); end; 




:: deftheorem    defines :::"R2Homeomorphism"::: TOPREALA:def 2 :  (Bool  "for" (Set (Var "b1")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set  ($#k3_topmetr :::"R^1"::: ) ) "," (Set  ($#k3_topmetr :::"R^1"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_topreala :::"R2Homeomorphism"::: )  )) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "b1"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )))  ")" )); 
 
theorem :: TOPREALA:33 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set (Set  ($#k2_topreala :::"R2Homeomorphism"::: ) )  ($#k7_relset_1 :::".:"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_card_3 :::"product"::: )  (Set  "("  "(" (Num 1) "," (Num 2) ")"   ($#k4_funct_4 :::"-->"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")"  ")" )))) ; 
 
theorem :: TOPREALA:34 (Bool (Set   ($#k2_topreala :::"R2Homeomorphism"::: )  ) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) ; 
 
theorem :: TOPREALA:35 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))) "holds"  (Bool (Set (Set  ($#k2_topreala :::"R2Homeomorphism"::: ) )  ($#k2_partfun1 :::"|"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" ) ($#k2_borsuk_1 :::":]"::: ) ))) "is"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set  "("  ($#k1_topreala :::"Trectangle"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "," (Set (Var "s")) ")"  ")" ))) ; 
 
theorem :: TOPREALA:36 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))) "holds"  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set  "("  ($#k1_topreala :::"Trectangle"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "," (Set (Var "s")) ")"  ")" )  "st" (Bool (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k2_topreala :::"R2Homeomorphism"::: ) )  ($#k2_partfun1 :::"|"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" ) ($#k2_borsuk_1 :::":]"::: ) ))))) "holds"  (Bool (Set (Var "h")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ))) ; 
 
theorem :: TOPREALA:37 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))) "holds"  (Bool (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set   ($#k1_topreala :::"Trectangle"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "," (Set (Var "s")) ")" )  ($#r1_t_0topsp :::"are_homeomorphic"::: )  )) ; 
 
theorem :: TOPREALA:38 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (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 "a")) "," (Set (Var "b")) ")"  ")" )  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" ) "holds"  (Bool (Set   ($#k4_card_3 :::"product"::: )  (Set  "("  "(" (Num 1) "," (Num 2) ")"   ($#k4_funct_4 :::"-->"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")"  ")" )) "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_topreala :::"Trectangle"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "," (Set (Var "s")) ")"  ")" ))))) ; 
 
theorem :: TOPREALA:39 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))) "holds"  (Bool  "for" (Set (Var "A")) "being"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" )  (Bool  "for" (Set (Var "B")) "being"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" ) "holds"  (Bool (Set   ($#k4_card_3 :::"product"::: )  (Set  "("  "(" (Num 1) "," (Num 2) ")"   ($#k4_funct_4 :::"-->"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")"  ")" )) "is"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_topreala :::"Trectangle"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "," (Set (Var "s")) ")"  ")" ))))) ; 
 
theorem :: TOPREALA:40 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))) "holds"  (Bool  "for" (Set (Var "A")) "being"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" )  (Bool  "for" (Set (Var "B")) "being"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "r")) "," (Set (Var "s")) ")"  ")" ) "holds"  (Bool (Set   ($#k4_card_3 :::"product"::: )  (Set  "("  "(" (Num 1) "," (Num 2) ")"   ($#k4_funct_4 :::"-->"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")"  ")" )) "is"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_topreala :::"Trectangle"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "r")) "," (Set (Var "s")) ")"  ")" ))))) ;