:: SPRECT_1 semantic presentation begin registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set ($#k5_numbers :::"NAT"::: ) )) ($#v1_funct_1 :::"Function-like"::: ) ($#v3_funct_1 :::"constant"::: ) bbbadV1_FINSET_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: SPRECT_1:1 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Set (Var "f")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "g"))) "is" ($#v3_funct_1 :::"constant"::: ) )) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_funct_1 :::"constant"::: ) ) & (Bool (Set (Var "g")) "is" ($#v3_funct_1 :::"constant"::: ) ) ")" )) ; theorem :: SPRECT_1:2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "is" ($#v3_funct_1 :::"constant"::: ) )) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ; theorem :: SPRECT_1:3 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k11_finseq_1 :::"*>"::: ) ) "is" ($#v3_funct_1 :::"constant"::: ) )) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "z"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )) ; begin theorem :: SPRECT_1:4 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "A")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: SPRECT_1:5 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "A")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))))) ; theorem :: SPRECT_1:6 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "," (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "B1")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Var "A"))) & (Bool (Set (Var "B2")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Var "A"))) & (Bool (Set (Var "S")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Var "A"))) & (Bool (Set (Set (Var "B1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B2"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Bool "not" (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Var "B1"))))) "holds" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Var "B2")))))) ; theorem :: SPRECT_1:7 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "," (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "B1")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Var "A"))) & (Bool (Set (Var "B2")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Var "A"))) & (Bool (Set (Var "C1")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Var "A"))) & (Bool (Set (Var "C2")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Var "A"))) & (Bool (Set (Set (Var "B1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B2"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set (Set (Var "C1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C2"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "B1")) "," (Set (Var "B2")) ($#k2_tarski :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "C1")) "," (Set (Var "C2")) ($#k2_tarski :::"}"::: ) ))))) ; begin theorem :: SPRECT_1:8 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" ")" )))) ; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "f" be ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); cluster (Set ($#k3_topreal1 :::"L~"::: ) "f") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "f" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); cluster (Set ($#k3_topreal1 :::"L~"::: ) "f") -> ($#v2_compts_1 :::"compact"::: ) ; end; theorem :: SPRECT_1:9 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) "is" ($#v1_sppol_1 :::"horizontal"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v1_sppol_1 :::"horizontal"::: ) )) ; theorem :: SPRECT_1:10 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) "is" ($#v2_sppol_1 :::"vertical"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v2_sppol_1 :::"vertical"::: ) )) ; registration cluster (Set ($#k1_topreal1 :::"R^2-unit_square"::: ) ) -> ($#v1_topreal4 :::"special_polygonal"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ))); end; begin theorem :: SPRECT_1:11 (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) ")" ) "holds" (Bool "(" (Bool (Set ($#k20_pscomp_1 :::"N-min"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set ($#k21_pscomp_1 :::"N-max"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) ")" )) ; theorem :: SPRECT_1:12 (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) ")" ) "holds" (Bool "(" (Bool (Set ($#k25_pscomp_1 :::"S-min"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set ($#k24_pscomp_1 :::"S-max"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) ")" )) ; theorem :: SPRECT_1:13 (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) ")" ) "holds" (Bool "(" (Bool (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set ($#k19_pscomp_1 :::"W-max"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) ")" )) ; theorem :: SPRECT_1:14 (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) ")" ) "holds" (Bool "(" (Bool (Set ($#k23_pscomp_1 :::"E-min"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) ")" )) ; theorem :: SPRECT_1:15 (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) ")" ) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v2_sppol_1 :::"vertical"::: ) ) "iff" (Bool (Set ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C")))) ")" )) ; theorem :: SPRECT_1: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) ")" ) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v1_sppol_1 :::"horizontal"::: ) ) "iff" (Bool (Set ($#k9_pscomp_1 :::"S-bound"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k7_pscomp_1 :::"N-bound"::: ) (Set (Var "C")))) ")" )) ; theorem :: SPRECT_1: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 ($#k11_pscomp_1 :::"NW-corner"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k12_pscomp_1 :::"NE-corner"::: ) (Set (Var "C"))))) "holds" (Bool (Set (Var "C")) "is" ($#v2_sppol_1 :::"vertical"::: ) )) ; theorem :: SPRECT_1:18 (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 ($#k10_pscomp_1 :::"SW-corner"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k13_pscomp_1 :::"SE-corner"::: ) (Set (Var "C"))))) "holds" (Bool (Set (Var "C")) "is" ($#v2_sppol_1 :::"vertical"::: ) )) ; theorem :: SPRECT_1:19 (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 ($#k11_pscomp_1 :::"NW-corner"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k10_pscomp_1 :::"SW-corner"::: ) (Set (Var "C"))))) "holds" (Bool (Set (Var "C")) "is" ($#v1_sppol_1 :::"horizontal"::: ) )) ; theorem :: SPRECT_1:20 (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 ($#k12_pscomp_1 :::"NE-corner"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k13_pscomp_1 :::"SE-corner"::: ) (Set (Var "C"))))) "holds" (Bool (Set (Var "C")) "is" ($#v1_sppol_1 :::"horizontal"::: ) )) ; theorem :: SPRECT_1:21 (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) ")" ) "holds" (Bool (Set ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C"))))) ; theorem :: SPRECT_1:22 (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) ")" ) "holds" (Bool (Set ($#k9_pscomp_1 :::"S-bound"::: ) (Set (Var "C"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_pscomp_1 :::"N-bound"::: ) (Set (Var "C"))))) ; theorem :: SPRECT_1:23 (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) ")" ) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k13_pscomp_1 :::"SE-corner"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k12_pscomp_1 :::"NE-corner"::: ) (Set (Var "C")) ")" ) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C")))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_pscomp_1 :::"N-bound"::: ) (Set (Var "C")))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k9_pscomp_1 :::"S-bound"::: ) (Set (Var "C")))) ")" ) "}" )) ; theorem :: SPRECT_1:24 (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) ")" ) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k10_pscomp_1 :::"SW-corner"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k13_pscomp_1 :::"SE-corner"::: ) (Set (Var "C")) ")" ) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C")))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C")))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k9_pscomp_1 :::"S-bound"::: ) (Set (Var "C")))) ")" ) "}" )) ; theorem :: SPRECT_1:25 (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) ")" ) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k11_pscomp_1 :::"NW-corner"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k12_pscomp_1 :::"NE-corner"::: ) (Set (Var "C")) ")" ) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C")))) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C")))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_pscomp_1 :::"N-bound"::: ) (Set (Var "C")))) ")" ) "}" )) ; theorem :: SPRECT_1:26 (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) ")" ) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k10_pscomp_1 :::"SW-corner"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k11_pscomp_1 :::"NW-corner"::: ) (Set (Var "C")) ")" ) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C")))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_pscomp_1 :::"N-bound"::: ) (Set (Var "C")))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k9_pscomp_1 :::"S-bound"::: ) (Set (Var "C")))) ")" ) "}" )) ; theorem :: SPRECT_1:27 (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) ")" ) "holds" (Bool (Set (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k10_pscomp_1 :::"SW-corner"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k11_pscomp_1 :::"NW-corner"::: ) (Set (Var "C")) ")" ) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k11_pscomp_1 :::"NW-corner"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k12_pscomp_1 :::"NE-corner"::: ) (Set (Var "C")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k11_pscomp_1 :::"NW-corner"::: ) (Set (Var "C")) ")" ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: SPRECT_1:28 (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) ")" ) "holds" (Bool (Set (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k11_pscomp_1 :::"NW-corner"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k12_pscomp_1 :::"NE-corner"::: ) (Set (Var "C")) ")" ) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k12_pscomp_1 :::"NE-corner"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k13_pscomp_1 :::"SE-corner"::: ) (Set (Var "C")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k12_pscomp_1 :::"NE-corner"::: ) (Set (Var "C")) ")" ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: SPRECT_1:29 (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) ")" ) "holds" (Bool (Set (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k13_pscomp_1 :::"SE-corner"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k12_pscomp_1 :::"NE-corner"::: ) (Set (Var "C")) ")" ) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k10_pscomp_1 :::"SW-corner"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k13_pscomp_1 :::"SE-corner"::: ) (Set (Var "C")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k13_pscomp_1 :::"SE-corner"::: ) (Set (Var "C")) ")" ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: SPRECT_1:30 (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) ")" ) "holds" (Bool (Set (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k11_pscomp_1 :::"NW-corner"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k10_pscomp_1 :::"SW-corner"::: ) (Set (Var "C")) ")" ) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k10_pscomp_1 :::"SW-corner"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k13_pscomp_1 :::"SE-corner"::: ) (Set (Var "C")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k10_pscomp_1 :::"SW-corner"::: ) (Set (Var "C")) ")" ) ($#k1_tarski :::"}"::: ) ))) ; begin theorem :: SPRECT_1:31 (Bool "for" (Set (Var "D1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "D1"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "D1"))))) ; theorem :: SPRECT_1:32 (Bool "for" (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k9_pscomp_1 :::"S-bound"::: ) (Set (Var "D2"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k7_pscomp_1 :::"N-bound"::: ) (Set (Var "D2"))))) ; theorem :: SPRECT_1:33 (Bool "for" (Set (Var "D1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k10_pscomp_1 :::"SW-corner"::: ) (Set (Var "D1")) ")" ) "," (Set "(" ($#k11_pscomp_1 :::"NW-corner"::: ) (Set (Var "D1")) ")" ) ")" ) ($#r1_subset_1 :::"misses"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k13_pscomp_1 :::"SE-corner"::: ) (Set (Var "D1")) ")" ) "," (Set "(" ($#k12_pscomp_1 :::"NE-corner"::: ) (Set (Var "D1")) ")" ) ")" ))) ; theorem :: SPRECT_1:34 (Bool "for" (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k10_pscomp_1 :::"SW-corner"::: ) (Set (Var "D2")) ")" ) "," (Set "(" ($#k13_pscomp_1 :::"SE-corner"::: ) (Set (Var "D2")) ")" ) ")" ) ($#r1_subset_1 :::"misses"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k11_pscomp_1 :::"NW-corner"::: ) (Set (Var "D2")) ")" ) "," (Set "(" ($#k12_pscomp_1 :::"NE-corner"::: ) (Set (Var "D2")) ")" ) ")" ))) ; begin definitionlet "C" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); func :::"SpStSeq"::: "C" -> ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) equals :: SPRECT_1:def 1 (Set (Set ($#k3_finseq_4 :::"<*"::: ) (Set "(" ($#k11_pscomp_1 :::"NW-corner"::: ) "C" ")" ) "," (Set "(" ($#k12_pscomp_1 :::"NE-corner"::: ) "C" ")" ) "," (Set "(" ($#k13_pscomp_1 :::"SE-corner"::: ) "C" ")" ) ($#k3_finseq_4 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set "(" ($#k10_pscomp_1 :::"SW-corner"::: ) "C" ")" ) "," (Set "(" ($#k11_pscomp_1 :::"NW-corner"::: ) "C" ")" ) ($#k2_finseq_4 :::"*>"::: ) )); end; :: deftheorem defines :::"SpStSeq"::: SPRECT_1:def 1 : (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_finseq_4 :::"<*"::: ) (Set "(" ($#k11_pscomp_1 :::"NW-corner"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k12_pscomp_1 :::"NE-corner"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k13_pscomp_1 :::"SE-corner"::: ) (Set (Var "C")) ")" ) ($#k3_finseq_4 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set "(" ($#k10_pscomp_1 :::"SW-corner"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k11_pscomp_1 :::"NW-corner"::: ) (Set (Var "C")) ")" ) ($#k2_finseq_4 :::"*>"::: ) )))); theorem :: SPRECT_1:35 (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "S")) ")" ) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k11_pscomp_1 :::"NW-corner"::: ) (Set (Var "S"))))) ; theorem :: SPRECT_1:36 (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "S")) ")" ) ($#k7_partfun1 :::"/."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k12_pscomp_1 :::"NE-corner"::: ) (Set (Var "S"))))) ; theorem :: SPRECT_1:37 (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "S")) ")" ) ($#k7_partfun1 :::"/."::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set ($#k13_pscomp_1 :::"SE-corner"::: ) (Set (Var "S"))))) ; theorem :: SPRECT_1:38 (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "S")) ")" ) ($#k7_partfun1 :::"/."::: ) (Num 4)) ($#r1_hidden :::"="::: ) (Set ($#k10_pscomp_1 :::"SW-corner"::: ) (Set (Var "S"))))) ; theorem :: SPRECT_1:39 (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "S")) ")" ) ($#k7_partfun1 :::"/."::: ) (Num 5)) ($#r1_hidden :::"="::: ) (Set ($#k11_pscomp_1 :::"NW-corner"::: ) (Set (Var "S"))))) ; theorem :: SPRECT_1:40 (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Num 5))) ; theorem :: SPRECT_1:41 (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k11_pscomp_1 :::"NW-corner"::: ) (Set (Var "S")) ")" ) "," (Set "(" ($#k12_pscomp_1 :::"NE-corner"::: ) (Set (Var "S")) ")" ) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k12_pscomp_1 :::"NE-corner"::: ) (Set (Var "S")) ")" ) "," (Set "(" ($#k13_pscomp_1 :::"SE-corner"::: ) (Set (Var "S")) ")" ) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k13_pscomp_1 :::"SE-corner"::: ) (Set (Var "S")) ")" ) "," (Set "(" ($#k10_pscomp_1 :::"SW-corner"::: ) (Set (Var "S")) ")" ) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k10_pscomp_1 :::"SW-corner"::: ) (Set (Var "S")) ")" ) "," (Set "(" ($#k11_pscomp_1 :::"NW-corner"::: ) (Set (Var "S")) ")" ) ")" ")" ) ")" )))) ; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); cluster (Set ($#k1_sprect_1 :::"SpStSeq"::: ) "D") -> ($#~v3_funct_1 "non" ($#v3_funct_1 :::"constant"::: ) ) ; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); cluster (Set ($#k1_sprect_1 :::"SpStSeq"::: ) "D") -> ($#~v3_funct_1 "non" ($#v3_funct_1 :::"constant"::: ) ) ; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); cluster (Set ($#k1_sprect_1 :::"SpStSeq"::: ) "D") -> ($#v1_finseq_6 :::"circular"::: ) ($#v1_topreal1 :::"special"::: ) ($#v2_topreal1 :::"unfolded"::: ) ($#v1_goboard5 :::"s.c.c."::: ) ($#v2_goboard5 :::"standard"::: ) ; end; theorem :: SPRECT_1:42 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_sppol_2 :::"[."::: ) (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "D")) ")" ) "," (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "D")) ")" ) "," (Set "(" ($#k9_pscomp_1 :::"S-bound"::: ) (Set (Var "D")) ")" ) "," (Set "(" ($#k7_pscomp_1 :::"N-bound"::: ) (Set (Var "D")) ")" ) ($#k1_sppol_2 :::".]"::: ) ))) ; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); let "f" be ($#v1_pscomp_1 :::"continuous"::: ) ($#m1_subset_1 :::"RealMap":::) "of" (Set (Const "T")); cluster (Set "f" ($#k7_relat_1 :::".:"::: ) "X") -> ($#v3_xxreal_2 :::"bounded_below"::: ) ; cluster (Set "f" ($#k7_relat_1 :::".:"::: ) "X") -> ($#v4_xxreal_2 :::"bounded_above"::: ) ; end; theorem :: SPRECT_1:43 (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" (Set ($#k4_pscomp_1 :::"proj1"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set (Var "S")) ")" )))) ; theorem :: SPRECT_1:44 (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k9_pscomp_1 :::"S-bound"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set (Var "S")) ")" )))) ; theorem :: SPRECT_1:45 (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k7_pscomp_1 :::"N-bound"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set (Var "S")) ")" )))) ; theorem :: SPRECT_1:46 (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" (Set ($#k4_pscomp_1 :::"proj1"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set (Var "S")) ")" )))) ; theorem :: SPRECT_1:47 (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "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 "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "C1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C2"))))) "holds" (Bool (Set ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xxreal_0 :::"min"::: ) "(" (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C1")) ")" ) "," (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C2")) ")" ) ")" )))) ; theorem :: SPRECT_1:48 (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "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 "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "C1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C2"))))) "holds" (Bool (Set ($#k9_pscomp_1 :::"S-bound"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xxreal_0 :::"min"::: ) "(" (Set "(" ($#k9_pscomp_1 :::"S-bound"::: ) (Set (Var "C1")) ")" ) "," (Set "(" ($#k9_pscomp_1 :::"S-bound"::: ) (Set (Var "C2")) ")" ) ")" )))) ; theorem :: SPRECT_1:49 (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "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 "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "C1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C2"))))) "holds" (Bool (Set ($#k7_pscomp_1 :::"N-bound"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set "(" ($#k7_pscomp_1 :::"N-bound"::: ) (Set (Var "C1")) ")" ) "," (Set "(" ($#k7_pscomp_1 :::"N-bound"::: ) (Set (Var "C2")) ")" ) ")" )))) ; theorem :: SPRECT_1:50 (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "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 "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "C1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C2"))))) "holds" (Bool (Set ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C1")) ")" ) "," (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C2")) ")" ) ")" )))) ; registrationlet "r1", "r2" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set bbbadK1_XXREAL_1("r1" "," "r2")) -> ($#v5_xxreal_2 :::"real-bounded"::: ) for ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; theorem :: SPRECT_1:51 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r2")))) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "r1")) "," (Set (Var "r2")) ($#k1_rcomp_1 :::".]"::: ) )) "iff" (Bool "ex" (Set (Var "s1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s1"))) & (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s1")) ($#k8_real_1 :::"*"::: ) (Set (Var "r1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "s1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "r2")) ")" ))) ")" )) ")" )) ; theorem :: SPRECT_1:52 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "q")) ($#k17_euclid :::"`1"::: ) ))) "holds" (Bool (Set (Set ($#k4_pscomp_1 :::"proj1"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "q")) ($#k17_euclid :::"`1"::: ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SPRECT_1:53 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "q")) ($#k18_euclid :::"`2"::: ) ))) "holds" (Bool (Set (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ")" ) "," (Set "(" (Set (Var "q")) ($#k18_euclid :::"`2"::: ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SPRECT_1:54 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "q")) ($#k17_euclid :::"`1"::: ) ))) "holds" (Bool (Set ($#k6_pscomp_1 :::"W-bound"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ))) ; theorem :: SPRECT_1:55 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "q")) ($#k18_euclid :::"`2"::: ) ))) "holds" (Bool (Set ($#k9_pscomp_1 :::"S-bound"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ))) ; theorem :: SPRECT_1:56 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "q")) ($#k18_euclid :::"`2"::: ) ))) "holds" (Bool (Set ($#k7_pscomp_1 :::"N-bound"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k18_euclid :::"`2"::: ) ))) ; theorem :: SPRECT_1:57 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "q")) ($#k17_euclid :::"`1"::: ) ))) "holds" (Bool (Set ($#k8_pscomp_1 :::"E-bound"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k17_euclid :::"`1"::: ) ))) ; theorem :: SPRECT_1:58 (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) ")" ) "holds" (Bool (Set ($#k6_pscomp_1 :::"W-bound"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "C")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C"))))) ; theorem :: SPRECT_1:59 (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) ")" ) "holds" (Bool (Set ($#k9_pscomp_1 :::"S-bound"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "C")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_pscomp_1 :::"S-bound"::: ) (Set (Var "C"))))) ; theorem :: SPRECT_1:60 (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) ")" ) "holds" (Bool (Set ($#k7_pscomp_1 :::"N-bound"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "C")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_pscomp_1 :::"N-bound"::: ) (Set (Var "C"))))) ; theorem :: SPRECT_1:61 (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) ")" ) "holds" (Bool (Set ($#k8_pscomp_1 :::"E-bound"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "C")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C"))))) ; theorem :: SPRECT_1:62 (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) ")" ) "holds" (Bool (Set ($#k11_pscomp_1 :::"NW-corner"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "C")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_pscomp_1 :::"NW-corner"::: ) (Set (Var "C"))))) ; theorem :: SPRECT_1:63 (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) ")" ) "holds" (Bool (Set ($#k12_pscomp_1 :::"NE-corner"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "C")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k12_pscomp_1 :::"NE-corner"::: ) (Set (Var "C"))))) ; theorem :: SPRECT_1:64 (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) ")" ) "holds" (Bool (Set ($#k10_pscomp_1 :::"SW-corner"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "C")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_pscomp_1 :::"SW-corner"::: ) (Set (Var "C"))))) ; theorem :: SPRECT_1:65 (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) ")" ) "holds" (Bool (Set ($#k13_pscomp_1 :::"SE-corner"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "C")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k13_pscomp_1 :::"SE-corner"::: ) (Set (Var "C"))))) ; theorem :: SPRECT_1:66 (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) ")" ) "holds" (Bool (Set ($#k14_pscomp_1 :::"W-most"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "C")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k10_pscomp_1 :::"SW-corner"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k11_pscomp_1 :::"NW-corner"::: ) (Set (Var "C")) ")" ) ")" ))) ; theorem :: SPRECT_1:67 (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) ")" ) "holds" (Bool (Set ($#k15_pscomp_1 :::"N-most"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "C")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k11_pscomp_1 :::"NW-corner"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k12_pscomp_1 :::"NE-corner"::: ) (Set (Var "C")) ")" ) ")" ))) ; theorem :: SPRECT_1:68 (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) ")" ) "holds" (Bool (Set ($#k17_pscomp_1 :::"S-most"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "C")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k10_pscomp_1 :::"SW-corner"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k13_pscomp_1 :::"SE-corner"::: ) (Set (Var "C")) ")" ) ")" ))) ; theorem :: SPRECT_1:69 (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) ")" ) "holds" (Bool (Set ($#k16_pscomp_1 :::"E-most"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "C")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k13_pscomp_1 :::"SE-corner"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k12_pscomp_1 :::"NE-corner"::: ) (Set (Var "C")) ")" ) ")" ))) ; theorem :: SPRECT_1:70 (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) ")" ) "holds" (Bool (Set (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k10_pscomp_1 :::"SW-corner"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k11_pscomp_1 :::"NW-corner"::: ) (Set (Var "C")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k9_pscomp_1 :::"S-bound"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k7_pscomp_1 :::"N-bound"::: ) (Set (Var "C")) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SPRECT_1:71 (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) ")" ) "holds" (Bool (Set (Set ($#k4_pscomp_1 :::"proj1"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k11_pscomp_1 :::"NW-corner"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k12_pscomp_1 :::"NE-corner"::: ) (Set (Var "C")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C")) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SPRECT_1:72 (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) ")" ) "holds" (Bool (Set (Set ($#k5_pscomp_1 :::"proj2"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k12_pscomp_1 :::"NE-corner"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k13_pscomp_1 :::"SE-corner"::: ) (Set (Var "C")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k9_pscomp_1 :::"S-bound"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k7_pscomp_1 :::"N-bound"::: ) (Set (Var "C")) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SPRECT_1:73 (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) ")" ) "holds" (Bool (Set (Set ($#k4_pscomp_1 :::"proj1"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" ($#k13_pscomp_1 :::"SE-corner"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k10_pscomp_1 :::"SW-corner"::: ) (Set (Var "C")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k6_pscomp_1 :::"W-bound"::: ) (Set (Var "C")) ")" ) "," (Set "(" ($#k8_pscomp_1 :::"E-bound"::: ) (Set (Var "C")) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SPRECT_1:74 (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) ")" ) "holds" (Bool (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "C")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_pscomp_1 :::"SW-corner"::: ) (Set (Var "C"))))) ; theorem :: SPRECT_1:75 (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) ")" ) "holds" (Bool (Set ($#k19_pscomp_1 :::"W-max"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "C")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_pscomp_1 :::"NW-corner"::: ) (Set (Var "C"))))) ; theorem :: SPRECT_1:76 (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) ")" ) "holds" (Bool (Set ($#k20_pscomp_1 :::"N-min"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "C")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_pscomp_1 :::"NW-corner"::: ) (Set (Var "C"))))) ; theorem :: SPRECT_1:77 (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) ")" ) "holds" (Bool (Set ($#k21_pscomp_1 :::"N-max"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "C")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k12_pscomp_1 :::"NE-corner"::: ) (Set (Var "C"))))) ; theorem :: SPRECT_1:78 (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) ")" ) "holds" (Bool (Set ($#k23_pscomp_1 :::"E-min"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "C")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k13_pscomp_1 :::"SE-corner"::: ) (Set (Var "C"))))) ; theorem :: SPRECT_1:79 (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) ")" ) "holds" (Bool (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "C")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k12_pscomp_1 :::"NE-corner"::: ) (Set (Var "C"))))) ; theorem :: SPRECT_1:80 (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) ")" ) "holds" (Bool (Set ($#k25_pscomp_1 :::"S-min"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "C")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_pscomp_1 :::"SW-corner"::: ) (Set (Var "C"))))) ; theorem :: SPRECT_1:81 (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) ")" ) "holds" (Bool (Set ($#k24_pscomp_1 :::"S-max"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set "(" ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "C")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k13_pscomp_1 :::"SE-corner"::: ) (Set (Var "C"))))) ; begin definitionlet "f" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); attr "f" is :::"rectangular"::: means :: SPRECT_1:def 2 (Bool "ex" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "f" ($#r1_hidden :::"="::: ) (Set ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D"))))); end; :: deftheorem defines :::"rectangular"::: SPRECT_1:def 2 : (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_sprect_1 :::"rectangular"::: ) ) "iff" (Bool "ex" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k1_sprect_1 :::"SpStSeq"::: ) (Set (Var "D"))))) ")" )); registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) ($#~v2_sppol_1 "non" ($#v2_sppol_1 :::"vertical"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); cluster (Set ($#k1_sprect_1 :::"SpStSeq"::: ) "D") -> ($#v1_sprect_1 :::"rectangular"::: ) ; end; registration cluster bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set ($#k5_numbers :::"NAT"::: ) )) bbbadV5_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ))) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v1_sprect_1 :::"rectangular"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )); end; theorem :: SPRECT_1:82 (Bool "for" (Set (Var "s")) "being" ($#v1_sprect_1 :::"rectangular"::: ) ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Num 5))) ; registration cluster ($#v1_sprect_1 :::"rectangular"::: ) -> ($#~v3_funct_1 "non" ($#v3_funct_1 :::"constant"::: ) ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )); end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_sprect_1 :::"rectangular"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finseq_6 :::"circular"::: ) ($#v1_topreal1 :::"special"::: ) ($#v2_topreal1 :::"unfolded"::: ) ($#v1_goboard5 :::"s.c.c."::: ) ($#v2_goboard5 :::"standard"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )); end; theorem :: SPRECT_1:83 (Bool "for" (Set (Var "s")) "being" ($#v1_sprect_1 :::"rectangular"::: ) ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "s")) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k20_pscomp_1 :::"N-min"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set (Var "s")) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k19_pscomp_1 :::"W-max"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "s")) ")" ))) ")" )) ; theorem :: SPRECT_1:84 (Bool "for" (Set (Var "s")) "being" ($#v1_sprect_1 :::"rectangular"::: ) ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "s")) ($#k7_partfun1 :::"/."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k21_pscomp_1 :::"N-max"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set (Var "s")) ($#k7_partfun1 :::"/."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k22_pscomp_1 :::"E-max"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "s")) ")" ))) ")" )) ; theorem :: SPRECT_1:85 (Bool "for" (Set (Var "s")) "being" ($#v1_sprect_1 :::"rectangular"::: ) ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "s")) ($#k7_partfun1 :::"/."::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set ($#k24_pscomp_1 :::"S-max"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set (Var "s")) ($#k7_partfun1 :::"/."::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set ($#k23_pscomp_1 :::"E-min"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "s")) ")" ))) ")" )) ; theorem :: SPRECT_1:86 (Bool "for" (Set (Var "s")) "being" ($#v1_sprect_1 :::"rectangular"::: ) ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "s")) ($#k7_partfun1 :::"/."::: ) (Num 4)) ($#r1_hidden :::"="::: ) (Set ($#k25_pscomp_1 :::"S-min"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set (Var "s")) ($#k7_partfun1 :::"/."::: ) (Num 4)) ($#r1_hidden :::"="::: ) (Set ($#k18_pscomp_1 :::"W-min"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "s")) ")" ))) ")" )) ; begin theorem :: SPRECT_1:87 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r2"))) & (Bool (Set (Var "s1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s2")))) "holds" (Bool (Set ($#k1_sppol_2 :::"[."::: ) (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "s1")) "," (Set (Var "s2")) ($#k1_sppol_2 :::".]"::: ) ) "is" ($#v1_jordan1 :::"Jordan"::: ) )) ; registrationlet "f" be ($#v1_sprect_1 :::"rectangular"::: ) ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); cluster (Set ($#k3_topreal1 :::"L~"::: ) "f") -> ($#v1_jordan1 :::"Jordan"::: ) ; end; definitionlet "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); redefine attr "S" is :::"Jordan"::: means :: SPRECT_1:def 3 (Bool "(" (Bool (Set "S" ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "ex" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set "S" ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")))) & (Bool (Set (Var "A1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A2"))) & (Bool (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A1")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A2")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A2")))) & (Bool (Set (Var "A1")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set "S" ($#k3_subset_1 :::"`"::: ) )) & (Bool (Set (Var "A2")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set "S" ($#k3_subset_1 :::"`"::: ) )) ")" )) ")" ); end; :: deftheorem defines :::"Jordan"::: SPRECT_1:def 3 : (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_jordan1 :::"Jordan"::: ) ) "iff" (Bool "(" (Bool (Set (Set (Var "S")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "ex" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Set (Var "S")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")))) & (Bool (Set (Var "A1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A2"))) & (Bool (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A1")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A2")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A2")))) & (Bool (Set (Var "A1")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Set (Var "S")) ($#k3_subset_1 :::"`"::: ) )) & (Bool (Set (Var "A2")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Set (Var "S")) ($#k3_subset_1 :::"`"::: ) )) ")" )) ")" ) ")" )); theorem :: SPRECT_1:88 (Bool "for" (Set (Var "f")) "being" ($#v1_sprect_1 :::"rectangular"::: ) ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k2_goboard9 :::"LeftComp"::: ) (Set (Var "f"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k3_goboard9 :::"RightComp"::: ) (Set (Var "f"))))) ; registrationlet "f" be ($#~v3_funct_1 "non" ($#v3_funct_1 :::"constant"::: ) ) ($#v2_goboard5 :::"standard"::: ) ($#m2_finseq_1 :::"special_circular_sequence":::); cluster (Set ($#k2_goboard9 :::"LeftComp"::: ) "f") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k3_goboard9 :::"RightComp"::: ) "f") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: SPRECT_1:89 (Bool "for" (Set (Var "f")) "being" ($#v1_sprect_1 :::"rectangular"::: ) ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k2_goboard9 :::"LeftComp"::: ) (Set (Var "f"))) ($#r1_hidden :::"<>"::: ) (Set ($#k3_goboard9 :::"RightComp"::: ) (Set (Var "f"))))) ;