:: SPRECT_4  semantic presentation begin  





theorem :: SPRECT_4:1 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"S-Sequence_in_R2":::)  (Bool  "for" (Set (Var "Q")) "being"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "Q"))) & (Bool (Bool  "not" (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set (Var "Q"))))) "holds"  (Bool (Set (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k3_jordan3 :::"R_Cut"::: )   "(" (Set (Var "f")) "," (Set  "("  ($#k1_jordan5c :::"First_Point"::: )   "(" (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ) "," (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1) ")" ) "," (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ) ")" ) "," (Set (Var "Q")) ")"  ")" ) ")"  ")" ) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set (Var "Q")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k1_jordan5c :::"First_Point"::: )   "(" (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ) "," (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1) ")" ) "," (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ) ")" ) "," (Set (Var "Q")) ")"  ")" ) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: SPRECT_4:2 (Bool  "for" (Set (Var "f")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v4_topreal1 :::"being_S-Seq"::: )  ) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )))) "holds"  (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k2_jordan3 :::"L_Cut"::: )   "(" (Set (Var "f")) "," (Set (Var "p")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) ; 
 
theorem :: SPRECT_4:3 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"S-Sequence_in_R2":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f")) "," (Set (Var "j")) "," (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ) ")"  ")" )))) "holds"  (Bool   ($#r1_jordan5c :::"LE"::: )  (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "j"))) "," (Set (Var "p")) "," (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f"))) "," (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1)) "," (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )))))) ; 
 
theorem :: SPRECT_4:4 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"S-Sequence_in_R2":::)  (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 "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_topreal1 :::"LSeg"::: )   "(" (Set (Var "f")) "," (Set (Var "j")) ")" )) & (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set (Var "p")) "," (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "j"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" ))) "holds"  (Bool   ($#r1_jordan5c :::"LE"::: )  (Set (Var "p")) "," (Set (Var "q")) "," (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f"))) "," (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1)) "," (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" )))))) ; 
 
theorem :: SPRECT_4:5 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"S-Sequence_in_R2":::)  (Bool  "for" (Set (Var "Q")) "being"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "Q"))) & (Bool (Bool  "not" (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r2_hidden :::"in"::: )  (Set (Var "Q"))))) "holds"  (Bool (Set (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k2_jordan3 :::"L_Cut"::: )   "(" (Set (Var "f")) "," (Set  "("  ($#k2_jordan5c :::"Last_Point"::: )   "(" (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ) "," (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1) ")" ) "," (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ) ")" ) "," (Set (Var "Q")) ")"  ")" ) ")"  ")" ) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set (Var "Q")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k2_jordan5c :::"Last_Point"::: )   "(" (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ) "," (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1) ")" ) "," (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ) ")" ) "," (Set (Var "Q")) ")"  ")" ) ($#k1_tarski :::"}"::: ) )))) ; 
 



theorem :: SPRECT_4:6 (Bool  "for" (Set (Var "f")) "being"  ($#~v3_funct_1  "non"   ($#v3_funct_1 :::"constant"::: )   )    ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"special_circular_sequence":::)  "holds" (Bool (Set   ($#k2_goboard9 :::"LeftComp"::: )  (Set (Var "f")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k3_goboard9 :::"RightComp"::: )  (Set (Var "f"))))) ;