:: TOPREAL2  semantic presentation begin  















theorem :: TOPREAL2:1 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) & (Bool (Set (Var "p1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_topreal1 :::"R^2-unit_square"::: )  )) & (Bool (Set (Var "p2"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_topreal1 :::"R^2-unit_square"::: )  ))) "holds"  (Bool  "ex" (Set (Var "P1")) "," (Set (Var "P2")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "P1"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "P2"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set   ($#k1_topreal1 :::"R^2-unit_square"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "P1"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "P2")))) & (Bool (Set (Set (Var "P1"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "P2")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k2_tarski :::"}"::: ) ))  ")" ))) ; 
 
theorem :: TOPREAL2:2 (Bool (Set   ($#k1_topreal1 :::"R^2-unit_square"::: )  ) "is"   ($#v2_compts_1 :::"compact"::: )  ) ; 
 
theorem :: TOPREAL2:3 (Bool  "for" (Set (Var "q1")) "," (Set (Var "q2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "Q")) "," (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "Q")) ")" ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "P")) ")" )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool (Set (Var "Q"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "q1")) "," (Set (Var "q2")))) "holds"  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "q1")))) & (Bool (Set (Var "p2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "q2"))))) "holds"  (Bool (Set (Var "P"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2"))))))) ; 
 definitionlet "P" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); attr "P" is  :::"being_simple_closed_curve":::  means :: TOPREAL2:def 1 (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set  ($#k1_topreal1 :::"R^2-unit_square"::: ) ) ")" ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  "P" ")" ) "st" (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  )); end; 




:: deftheorem    defines :::"being_simple_closed_curve"::: TOPREAL2:def 1 :  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "P")) "is"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )  ) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set  ($#k1_topreal1 :::"R^2-unit_square"::: ) ) ")" ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "P")) ")" ) "st" (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ))  ")" )); 
 registration
cluster (Set   ($#k1_topreal1 :::"R^2-unit_square"::: )  ) ->   ($#v1_topreal2 :::"being_simple_closed_curve"::: )   ; 
end; registration
cluster   ($#v4_funct_1 :::"functional"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_topreal2 :::"being_simple_closed_curve"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))); 
end; definitionmode Simple_closed_curve is   ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ); end; 
theorem :: TOPREAL2:4 (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "P")) "is"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )  )) "holds"  (Bool  "ex" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) & (Bool (Set (Var "p1"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "p2"))  ($#r2_hidden :::"in"::: )  (Set (Var "P")))  ")" ))) ; 
 
theorem :: TOPREAL2:5 (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "P")) "is"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )  ) "iff" (Bool  "("  (Bool  "ex" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) & (Bool (Set (Var "p1"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "p2"))  ($#r2_hidden :::"in"::: )  (Set (Var "P")))  ")" )) & (Bool  "("   "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) & (Bool (Set (Var "p1"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "p2"))  ($#r2_hidden :::"in"::: )  (Set (Var "P")))) "holds"  (Bool  "ex" (Set (Var "P1")) "," (Set (Var "P2")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "P1"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "P2"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "P1"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "P2")))) & (Bool (Set (Set (Var "P1"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "P2")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k2_tarski :::"}"::: ) ))  ")" ))  ")" )  ")" )  ")" )) ; 
 
theorem :: TOPREAL2:6 (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "P")) "is"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )  ) "iff" (Bool  "ex" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )(Bool  "ex" (Set (Var "P1")) "," (Set (Var "P2")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" ) "st"  (Bool  "("  (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) & (Bool (Set (Var "p1"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "p2"))  ($#r2_hidden :::"in"::: )  (Set (Var "P"))) & (Bool (Set (Var "P1"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "P2"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "P1"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "P2")))) & (Bool (Set (Set (Var "P1"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "P2")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k2_tarski :::"}"::: ) ))  ")" )))  ")" )) ; 
 registration
cluster   ($#v1_topreal2 :::"being_simple_closed_curve"::: )    ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )))); 
end;