:: TOPREAL5 semantic presentation begin theorem :: TOPREAL5:1 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B1")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "B2")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "B1")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "A"))) & (Bool (Set (Var "B2")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B2")))) & (Bool (Set (Var "B1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B2")))) "holds" (Bool "not" (Bool (Set (Var "A")) "is" ($#v2_connsp_1 :::"connected"::: ) )))) ; theorem :: TOPREAL5:2 (Bool "for" (Set (Var "ra")) "," (Set (Var "rb")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "ra")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "rb")))) "holds" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "ra")) "," (Set (Var "rb")) ")" ")" )) "is" ($#v2_connsp_1 :::"connected"::: ) )) ; theorem :: TOPREAL5:3 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) & (Bool "ex" (Set (Var "b")) "," (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d"))) ")" ))) "holds" (Bool "not" (Bool (Set (Var "A")) "is" ($#v2_connsp_1 :::"connected"::: ) )))) ; theorem :: TOPREAL5:4 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "xa")) "," (Set (Var "xb")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_connsp_1 :::"connected"::: ) ) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "xa"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "xb"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d"))) & (Bool (Set (Var "d")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b")))) "holds" (Bool "ex" (Set (Var "xc")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "xc"))) ($#r1_hidden :::"="::: ) (Set (Var "d")))))))) ; theorem :: TOPREAL5:5 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "xa")) "," (Set (Var "xb")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool (Bool (Set (Var "B")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "xa"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "xb"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d"))) & (Bool (Set (Var "d")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "xa")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "xb")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "ex" (Set (Var "xc")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "xc")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "xc"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))) ")" ))))))) ; theorem :: TOPREAL5:6 (Bool "for" (Set (Var "ra")) "," (Set (Var "rb")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "ra")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "rb")))) "holds" (Bool "for" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "ra")) "," (Set (Var "rb")) ")" ")" ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "ra"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "rb"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d"))) & (Bool (Set (Var "d")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b")))) "holds" (Bool "ex" (Set (Var "rc")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "rc"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))) & (Bool (Set (Var "ra")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "rc"))) & (Bool (Set (Var "rc")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "rb"))) ")" ))))) ; theorem :: TOPREAL5:7 (Bool "for" (Set (Var "ra")) "," (Set (Var "rb")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "ra")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "rb")))) "holds" (Bool "for" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "ra")) "," (Set (Var "rb")) ")" ")" ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "ra"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "rb"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "d"))) & (Bool (Set (Var "d")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "b")))) "holds" (Bool "ex" (Set (Var "rc")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "rc"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))) & (Bool (Set (Var "ra")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "rc"))) & (Bool (Set (Var "rc")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "rb"))) ")" ))))) ; theorem :: TOPREAL5:8 (Bool "for" (Set (Var "ra")) "," (Set (Var "rb")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "ra")) "," (Set (Var "rb")) ")" ")" ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "ra")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "rb"))) & (Bool (Set (Set (Var "s1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "s2"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "ra")))) & (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "rb"))))) "holds" (Bool "ex" (Set (Var "r1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "r1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "ra")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r1"))) & (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "rb"))) ")" ))))) ; theorem :: TOPREAL5:9 (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1)))) "holds" (Bool "ex" (Set (Var "r1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r1"))) & (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "r1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "s2")) ")" ) ($#k6_real_1 :::"/"::: ) (Num 2))) ")" )))) ; begin theorem :: TOPREAL5:10 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k4_pscomp_1 :::"proj1"::: ) ))) "holds" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )) ; theorem :: TOPREAL5:11 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k5_pscomp_1 :::"proj2"::: ) ))) "holds" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )) ; theorem :: TOPREAL5:12 (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) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool "(" (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "r"))))) "holds" (Bool (Set (Set (Var "q")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "r"))))) ")" ) ")" )))) ; theorem :: TOPREAL5:13 (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) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ($#k1_pre_topc :::"|"::: ) (Set (Var "P")) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool "(" (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "r"))))) "holds" (Bool (Set (Set (Var "q")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "r"))))) ")" ) ")" )))) ; theorem :: TOPREAL5:14 (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 "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Bool "not" (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "r")))) ")" )))) ; theorem :: TOPREAL5:15 (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 "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Bool "not" (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "r")))) ")" )))) ; theorem :: TOPREAL5:16 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "C")) "is" ($#v1_topreal2 :::"being_simple_closed_curve"::: ) )) "holds" (Bool (Set ($#k7_pscomp_1 :::"N-bound"::: ) (Set (Var "C"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k9_pscomp_1 :::"S-bound"::: ) (Set (Var "C"))))) ; theorem :: TOPREAL5:17 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "C")) "is" ($#v1_topreal2 :::"being_simple_closed_curve"::: ) )) "holds" (Bool (Set ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C"))))) ; theorem :: TOPREAL5:18 (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#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 (Set ($#k25_pscomp_1 :::"S-min"::: ) (Set (Var "P"))) ($#r1_hidden :::"<>"::: ) (Set ($#k21_pscomp_1 :::"N-max"::: ) (Set (Var "P"))))) ; theorem :: TOPREAL5:19 (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#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 (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "P"))) ($#r1_hidden :::"<>"::: ) (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "P"))))) ; registration cluster ($#v1_topreal2 :::"being_simple_closed_curve"::: ) -> ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) 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;