:: SPPOL_1 semantic presentation begin theorem :: SPPOL_1:1 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "holds" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "k")) ($#k5_real_1 :::"-"::: ) (Num 1)))) ; theorem :: SPPOL_1:2 (Bool "for" (Set (Var "k")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "k")) ($#k9_real_1 :::"-"::: ) (Set (Var "m")))) & (Bool (Set (Set (Var "k")) ($#k9_real_1 :::"-"::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool "(" (Bool (Set (Set (Var "k")) ($#k9_real_1 :::"-"::: ) (Set (Var "m"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "k")) ($#k9_real_1 :::"-"::: ) (Set (Var "m"))) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )) ")" )) ; scheme :: SPPOL_1:sch 1 FinSeqFam{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set F1 "(" ")" ), F3( ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set F1 "(" ")" ) "," ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"Nat":::)] } : (Bool "{" (Set F3 "(" (Set F2 "(" ")" ) "," (Set (Var "i")) ")" ) where i "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set F2 "(" ")" ))) & (Bool P1[(Set (Var "i"))]) ")" ) "}" "is" ($#v1_finset_1 :::"finite"::: ) ) proof end; scheme :: SPPOL_1:sch 2 FinSeqFam9{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set F1 "(" ")" ), F3( ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set F1 "(" ")" ) "," ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set F3 "(" (Set F2 "(" ")" ) "," (Set (Var "i")) ")" ) where i "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set F2 "(" ")" ))) & (Bool P1[(Set (Var "i"))]) ")" ) "}" "is" ($#v1_finset_1 :::"finite"::: ) ) proof end; theorem :: SPPOL_1:3 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x1")) ($#k8_euclid :::"-"::: ) (Set (Var "x2")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k9_real_1 :::"-"::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x3")) ")" ) ($#k12_euclid :::".|"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x1")) ($#k8_euclid :::"-"::: ) (Set (Var "x3")) ")" ) ($#k12_euclid :::".|"::: ) )))) ; theorem :: SPPOL_1:4 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x1")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#k9_real_1 :::"-"::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x2")) ($#k8_euclid :::"-"::: ) (Set (Var "x3")) ")" ) ($#k12_euclid :::".|"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x3")) ($#k8_euclid :::"-"::: ) (Set (Var "x1")) ")" ) ($#k12_euclid :::".|"::: ) )))) ; begin theorem :: SPPOL_1:5 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "u1")) "," (Set (Var "u2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "u1"))) & (Bool (Set (Var "v2")) ($#r1_hidden :::"="::: ) (Set (Var "u2")))) "holds" (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "u1")) "," (Set (Var "u2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "v1")) ($#k8_euclid :::"-"::: ) (Set (Var "v2")) ")" ) ($#k12_euclid :::".|"::: ) ))))) ; theorem :: SPPOL_1:6 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "P")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ))) "holds" (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "s")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "s")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p2")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool (Set (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "r")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p2")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) ")" ) ")" ))))) ; theorem :: SPPOL_1:7 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) ")" )) & (Bool (Bool "not" (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Var "q1"))))) "holds" (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Var "q2"))))) ; theorem :: SPPOL_1:8 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" "not" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) ")" )) "or" (Bool "(" (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Var "q1"))) & (Bool (Set (Var "p2")) ($#r1_hidden :::"="::: ) (Set (Var "q2"))) ")" ) "or" (Bool "(" (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Var "q2"))) & (Bool (Set (Var "p2")) ($#r1_hidden :::"="::: ) (Set (Var "q1"))) ")" ) ")" ))) ; registrationlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "p1", "p2" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); cluster (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" "p1" "," "p2" ")" ) -> ($#v2_compts_1 :::"compact"::: ) ; cluster (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" "p1" "," "p2" ")" ) -> ($#v4_pre_topc :::"closed"::: ) ; end; definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "p" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); pred "p" :::"is_extremal_in"::: "P" means :: SPPOL_1:def 1 (Bool "(" (Bool "p" ($#r2_hidden :::"in"::: ) "P") & (Bool "(" "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) "st" (Bool (Bool "p" ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ) ($#r1_tarski :::"c="::: ) "P") & (Bool (Bool "not" "p" ($#r1_hidden :::"="::: ) (Set (Var "p1"))))) "holds" (Bool "p" ($#r1_hidden :::"="::: ) (Set (Var "p2"))) ")" ) ")" ); end; :: deftheorem defines :::"is_extremal_in"::: SPPOL_1:def 1 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_sppol_1 :::"is_extremal_in"::: ) (Set (Var "P"))) "iff" (Bool "(" (Bool (Set (Var "p")) ($#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"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Bool "not" (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p1"))))) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p2"))) ")" ) ")" ) ")" )))); theorem :: SPPOL_1:9 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_sppol_1 :::"is_extremal_in"::: ) (Set (Var "P"))) & (Bool (Set (Var "Q")) ($#r1_tarski :::"c="::: ) (Set (Var "P"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "Q")))) "holds" (Bool (Set (Var "p")) ($#r1_sppol_1 :::"is_extremal_in"::: ) (Set (Var "Q")))))) ; theorem :: SPPOL_1:10 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Var "p")) ($#r1_sppol_1 :::"is_extremal_in"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: SPPOL_1:11 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Var "p1")) ($#r1_sppol_1 :::"is_extremal_in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )))) ; theorem :: SPPOL_1:12 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p2")) "," (Set (Var "p1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set (Var "p2")) ($#r1_sppol_1 :::"is_extremal_in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )))) ; theorem :: SPPOL_1:13 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" "not" (Bool (Set (Var "p")) ($#r1_sppol_1 :::"is_extremal_in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) "or" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) "or" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p2"))) ")" ))) ; begin theorem :: SPPOL_1:14 (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 (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set (Var "p1")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "p2")) ($#k18_euclid :::"`2"::: ) ))) "holds" (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 ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "p1")) ($#k18_euclid :::"`2"::: ) )) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "p2")) ($#k18_euclid :::"`2"::: ) )) ")" ))) ; definitionlet "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); attr "P" is :::"horizontal"::: means :: SPPOL_1:def 2 (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 (Var "p")) ($#r2_hidden :::"in"::: ) "P") & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "P")) "holds" (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k18_euclid :::"`2"::: ) ))); attr "P" is :::"vertical"::: means :: SPPOL_1:def 3 (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 (Var "p")) ($#r2_hidden :::"in"::: ) "P") & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "P")) "holds" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k17_euclid :::"`1"::: ) ))); end; :: deftheorem defines :::"horizontal"::: SPPOL_1:def 2 : (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_sppol_1 :::"horizontal"::: ) ) "iff" (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 (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k18_euclid :::"`2"::: ) ))) ")" )); :: deftheorem defines :::"vertical"::: SPPOL_1:def 3 : (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" ($#v2_sppol_1 :::"vertical"::: ) ) "iff" (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 (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k17_euclid :::"`1"::: ) ))) ")" )); registration cluster ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#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) ")" ))); cluster ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#v2_sppol_1 :::"vertical"::: ) -> ($#~v1_sppol_1 "non" ($#v1_sppol_1 :::"horizontal"::: ) ) 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; theorem :: SPPOL_1:15 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k18_euclid :::"`2"::: ) )) "iff" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) "is" ($#v1_sppol_1 :::"horizontal"::: ) ) ")" )) ; theorem :: SPPOL_1:16 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k17_euclid :::"`1"::: ) )) "iff" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) "is" ($#v2_sppol_1 :::"vertical"::: ) ) ")" )) ; theorem :: SPPOL_1:17 (Bool "for" (Set (Var "p1")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )) & (Bool (Set (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set (Var "p1")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p2")) ($#k18_euclid :::"`2"::: ) ))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) "is" ($#v1_sppol_1 :::"horizontal"::: ) )) ; theorem :: SPPOL_1:18 (Bool "for" (Set (Var "p1")) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )) & (Bool (Set (Set (Var "p1")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "p2")) ($#k18_euclid :::"`2"::: ) )) & (Bool (Set (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) ))) "holds" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) "is" ($#v2_sppol_1 :::"vertical"::: ) )) ; registrationlet "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )); let "i" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k2_topreal1 :::"LSeg"::: ) "(" "f" "," "i" ")" ) -> ($#v4_pre_topc :::"closed"::: ) ; end; theorem :: SPPOL_1:19 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) "holds" (Bool "(" "not" (Bool (Set (Var "f")) "is" ($#v1_topreal1 :::"special"::: ) ) "or" (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ) "is" ($#v2_sppol_1 :::"vertical"::: ) ) "or" (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ) "is" ($#v1_sppol_1 :::"horizontal"::: ) ) ")" ))) ; theorem :: SPPOL_1:20 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool "not" (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ) "is" ($#v1_zfmisc_1 :::"trivial"::: ) )))) ; theorem :: SPPOL_1:21 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ) "is" ($#v2_sppol_1 :::"vertical"::: ) )) "holds" (Bool "not" (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ) "is" ($#v1_sppol_1 :::"horizontal"::: ) )))) ; theorem :: SPPOL_1:22 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) "holds" (Bool "{" (Set "(" ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ")" ) where i "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) ")" ) "}" "is" ($#v1_finset_1 :::"finite"::: ) )) ; theorem :: SPPOL_1:23 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) "holds" (Bool "{" (Set "(" ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ")" ) where i "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) ")" ) "}" "is" ($#v1_finset_1 :::"finite"::: ) )) ; theorem :: SPPOL_1:24 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) "holds" (Bool "{" (Set "(" ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ")" ) where i "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) ")" ) "}" "is" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ))) ; theorem :: SPPOL_1:25 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) "holds" (Bool "{" (Set "(" ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ")" ) where i "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) ")" ) "}" "is" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ))) ; theorem :: SPPOL_1:26 (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) "st" (Bool (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ")" ) where i "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) ")" ) "}" ))) "holds" (Bool (Set (Var "Q")) "is" ($#v4_pre_topc :::"closed"::: ) ))) ; registrationlet "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )); cluster (Set ($#k3_topreal1 :::"L~"::: ) "f") -> ($#v4_pre_topc :::"closed"::: ) ; end; definitionlet "IT" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); attr "IT" is :::"alternating"::: means :: SPPOL_1:def 4 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "IT"))) "holds" (Bool "(" (Bool (Set (Set "(" "IT" ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set "(" "IT" ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set "(" "IT" ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set "(" "IT" ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k18_euclid :::"`2"::: ) )) ")" )); end; :: deftheorem defines :::"alternating"::: SPPOL_1:def 4 : (Bool "for" (Set (Var "IT")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_sppol_1 :::"alternating"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "IT"))))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "IT")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set "(" (Set (Var "IT")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set "(" (Set (Var "IT")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set "(" (Set (Var "IT")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k18_euclid :::"`2"::: ) )) ")" )) ")" )); theorem :: SPPOL_1:27 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_topreal1 :::"special"::: ) ) & (Bool (Set (Var "f")) "is" ($#v3_sppol_1 :::"alternating"::: ) ) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k17_euclid :::"`1"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k18_euclid :::"`2"::: ) )))) ; theorem :: SPPOL_1:28 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_topreal1 :::"special"::: ) ) & (Bool (Set (Var "f")) "is" ($#v3_sppol_1 :::"alternating"::: ) ) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k18_euclid :::"`2"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k17_euclid :::"`1"::: ) )))) ; theorem :: SPPOL_1:29 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_topreal1 :::"special"::: ) ) & (Bool (Set (Var "f")) "is" ($#v3_sppol_1 :::"alternating"::: ) ) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")))) & (Bool (Set (Var "p2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Var "p3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ))) & (Bool "not" (Bool "(" (Bool (Set (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set (Var "p3")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) )) ")" ))) "holds" (Bool "(" (Bool (Set (Set (Var "p1")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p2")) ($#k18_euclid :::"`2"::: ) )) & (Bool (Set (Set (Var "p3")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "p2")) ($#k18_euclid :::"`2"::: ) )) ")" )))) ; theorem :: SPPOL_1:30 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_topreal1 :::"special"::: ) ) & (Bool (Set (Var "f")) "is" ($#v3_sppol_1 :::"alternating"::: ) ) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")))) & (Bool (Set (Var "p2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Var "p3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ))) & (Bool "not" (Bool "(" (Bool (Set (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p3")) ($#k17_euclid :::"`1"::: ) )) & (Bool (Set (Set (Var "p1")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "p2")) ($#k17_euclid :::"`1"::: ) )) ")" ))) "holds" (Bool "(" (Bool (Set (Set (Var "p2")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p3")) ($#k18_euclid :::"`2"::: ) )) & (Bool (Set (Set (Var "p1")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "p2")) ($#k18_euclid :::"`2"::: ) )) ")" )))) ; theorem :: SPPOL_1:31 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_topreal1 :::"special"::: ) ) & (Bool (Set (Var "f")) "is" ($#v3_sppol_1 :::"alternating"::: ) ) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool "not" (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )))))) ; theorem :: SPPOL_1:32 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_topreal1 :::"special"::: ) ) & (Bool (Set (Var "f")) "is" ($#v3_sppol_1 :::"alternating"::: ) ) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ) "is" ($#v2_sppol_1 :::"vertical"::: ) )) "holds" (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "is" ($#v1_sppol_1 :::"horizontal"::: ) ))) ; theorem :: SPPOL_1:33 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_topreal1 :::"special"::: ) ) & (Bool (Set (Var "f")) "is" ($#v3_sppol_1 :::"alternating"::: ) ) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ) "is" ($#v1_sppol_1 :::"horizontal"::: ) )) "holds" (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "is" ($#v2_sppol_1 :::"vertical"::: ) ))) ; theorem :: SPPOL_1:34 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_topreal1 :::"special"::: ) ) & (Bool (Set (Var "f")) "is" ($#v3_sppol_1 :::"alternating"::: ) ) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool "not" (Bool "(" (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ) "is" ($#v2_sppol_1 :::"vertical"::: ) ) & (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "is" ($#v1_sppol_1 :::"horizontal"::: ) ) ")" ))) "holds" (Bool "(" (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ) "is" ($#v1_sppol_1 :::"horizontal"::: ) ) & (Bool (Set ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "is" ($#v2_sppol_1 :::"vertical"::: ) ) ")" ))) ; theorem :: SPPOL_1:35 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) (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 (Var "f")) "is" ($#v1_topreal1 :::"special"::: ) ) & (Bool (Set (Var "f")) "is" ($#v3_sppol_1 :::"alternating"::: ) ) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )) & (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ))) & (Bool (Bool "not" (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "q")))))) ; theorem :: SPPOL_1:36 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_topreal1 :::"special"::: ) ) & (Bool (Set (Var "f")) "is" ($#v3_sppol_1 :::"alternating"::: ) ) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_sppol_1 :::"is_extremal_in"::: ) (Set (Set "(" ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ))))) ; theorem :: SPPOL_1:37 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_topreal1 :::"special"::: ) ) & (Bool (Set (Var "f")) "is" ($#v3_sppol_1 :::"alternating"::: ) ) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Bool "not" (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ))))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "s")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "p3")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Bool "not" (Set (Var "p3")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_topreal1 :::"LSeg"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )))) & (Bool (Set (Var "p3")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )) & (Bool (Set (Var "p3")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "u")) "," (Set (Var "s")) ")" )) ")" ))))))) ; definitionlet "f1", "f2" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )); let "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ); pred "f1" "," "f2" :::"are_generators_of"::: "P" means :: SPPOL_1:def 5 (Bool "(" (Bool "f1" "is" ($#v3_sppol_1 :::"alternating"::: ) ) & (Bool "f1" "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool "f2" "is" ($#v3_sppol_1 :::"alternating"::: ) ) & (Bool "f2" "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set "f1" ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set "f2" ($#k7_partfun1 :::"/."::: ) (Num 1))) & (Bool (Set "f1" ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "f1" ")" )) ($#r1_hidden :::"="::: ) (Set "f2" ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "f2" ")" ))) & (Bool (Set ($#k3_finseq_4 :::"<*"::: ) (Set "(" "f1" ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) "," (Set "(" "f1" ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," (Set "(" "f2" ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) ($#k3_finseq_4 :::"*>"::: ) ) "is" ($#v3_sppol_1 :::"alternating"::: ) ) & (Bool (Set ($#k3_finseq_4 :::"<*"::: ) (Set "(" "f1" ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) "f1" ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ")" ) "," (Set "(" "f1" ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "f1" ")" ) ")" ) "," (Set "(" "f2" ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) "f2" ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ")" ) ($#k3_finseq_4 :::"*>"::: ) ) "is" ($#v3_sppol_1 :::"alternating"::: ) ) & (Bool (Set "f1" ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"<>"::: ) (Set "f1" ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "f1" ")" ))) & (Bool (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) "f1" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) "f2" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set "(" "f1" ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," (Set "(" "f1" ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "f1" ")" ) ")" ) ($#k7_domain_1 :::"}"::: ) )) & (Bool "P" ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) "f1" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) "f2" ")" ))) ")" ); end; :: deftheorem defines :::"are_generators_of"::: SPPOL_1:def 5 : (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "f1")) "," (Set (Var "f2")) ($#r2_sppol_1 :::"are_generators_of"::: ) (Set (Var "P"))) "iff" (Bool "(" (Bool (Set (Var "f1")) "is" ($#v3_sppol_1 :::"alternating"::: ) ) & (Bool (Set (Var "f1")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v3_sppol_1 :::"alternating"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v4_topreal1 :::"being_S-Seq"::: ) ) & (Bool (Set (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k7_partfun1 :::"/."::: ) (Num 1))) & (Bool (Set (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f2")) ")" ))) & (Bool (Set ($#k3_finseq_4 :::"<*"::: ) (Set "(" (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) "," (Set "(" (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "f2")) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) ($#k3_finseq_4 :::"*>"::: ) ) "is" ($#v3_sppol_1 :::"alternating"::: ) ) & (Bool (Set ($#k3_finseq_4 :::"<*"::: ) (Set "(" (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1")) ")" ) ")" ) "," (Set "(" (Set (Var "f2")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f2")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ")" ) ($#k3_finseq_4 :::"*>"::: ) ) "is" ($#v3_sppol_1 :::"alternating"::: ) ) & (Bool (Set (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1")) ")" ))) & (Bool (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set "(" (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1")) ")" ) ")" ) ($#k7_domain_1 :::"}"::: ) )) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_topreal1 :::"L~"::: ) (Set (Var "f2")) ")" ))) ")" ) ")" ))); theorem :: SPPOL_1:38 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) "st" (Bool (Bool (Set (Var "f1")) "," (Set (Var "f2")) ($#r2_sppol_1 :::"are_generators_of"::: ) (Set (Var "P"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1"))))) "holds" (Bool (Set (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_sppol_1 :::"is_extremal_in"::: ) (Set (Var "P")))))) ; theorem :: SPPOL_1:39 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "p9")) "," (Set (Var "q9")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "p9"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "q9")))) "holds" (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "p9")) "," (Set (Var "q9")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "q")) ")" ) ($#k12_euclid :::".|"::: ) ))))) ; theorem :: SPPOL_1:40 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) "is" ($#v1_sppol_1 :::"horizontal"::: ) ) & (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ))) "holds" (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k18_euclid :::"`2"::: ) ))) ; theorem :: SPPOL_1:41 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) "is" ($#v2_sppol_1 :::"vertical"::: ) ) & (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ))) "holds" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k17_euclid :::"`1"::: ) ))) ; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_funct_1 :::"functional"::: ) ($#v2_compts_1 :::"compact"::: ) ($#v1_sppol_1 :::"horizontal"::: ) 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) ")" ))); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_funct_1 :::"functional"::: ) ($#v2_compts_1 :::"compact"::: ) ($#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;