:: JORDAN1G  semantic presentation begin  


registration
cluster   ($#v1_zfmisc_1 :::"trivial"::: )   bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set   ($#k5_numbers :::"NAT"::: )  ))   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FINSET_1()   ($#v1_finseq_1 :::"FinSequence-like"::: )     ($#v2_finseq_1 :::"FinSubsequence-like"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: JORDAN1G:1 (Bool  "for" (Set (Var "f")) "being"   ($#v1_zfmisc_1 :::"trivial"::: )    ($#m1_hidden :::"FinSequence":::)  "holds"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v1_xboole_0 :::"empty"::: )  ) "or" (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) )))  ")" )) ; 
 registrationlet "p" be  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )   ($#m1_hidden :::"FinSequence":::); 
cluster (Set   ($#k3_finseq_5 :::"Rev"::: )  "p") ->  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )  ; 
end; 
theorem :: JORDAN1G:2 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D"))  (Bool  "for" (Set (Var "p")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "f"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "G")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_finseq_5 :::"-:"::: )  (Set (Var "p")))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "G"))))))) ; 
 
theorem :: JORDAN1G:3 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "G")) "being"   ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "D"))  (Bool  "for" (Set (Var "p")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "D"))  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))) & (Bool (Set (Var "f"))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "G")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_finseq_5 :::":-"::: )  (Set (Var "p")))  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set (Var "G"))))))) ; 
 
theorem :: JORDAN1G:4 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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   ($#k1_jordan1e :::"Upper_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")" )  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set   ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")" )))) ; 
 
theorem :: JORDAN1G:5 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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   ($#k2_jordan1e :::"Lower_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")" )  ($#r1_goboard1 :::"is_sequence_on"::: )  (Set   ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")" )))) ; 
 registrationlet "C" be   ($#v2_connsp_1 :::"connected"::: )     ($#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) ")" ); let "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k1_jordan1e :::"Upper_Seq"::: )   "(" "C" "," "n" ")" ) ->   ($#v2_goboard5 :::"standard"::: )   ; 

cluster (Set   ($#k2_jordan1e :::"Lower_Seq"::: )   "(" "C" "," "n" ")" ) ->   ($#v2_goboard5 :::"standard"::: )   ; 
end; 
theorem :: JORDAN1G:6 (Bool  "for" (Set (Var "G")) "being"   ($#v3_goboard1 :::"Y_equal-in-column"::: )     ($#v4_goboard1 :::"Y_increasing-in-line"::: )    ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "j1")) "," (Set (Var "j2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set (Var "G")))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set (Var "G")))) & (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i1")) "," (Set (Var "j1")) ")"  ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i2")) "," (Set (Var "j2")) ")"  ")" )  ($#k18_euclid :::"`2"::: )  ))) "holds"  (Bool (Set (Var "j1"))  ($#r1_hidden :::"="::: )  (Set (Var "j2"))))) ; 
 
theorem :: JORDAN1G:7 (Bool  "for" (Set (Var "G")) "being"   ($#v2_goboard1 :::"X_equal-in-line"::: )     ($#v5_goboard1 :::"X_increasing-in-column"::: )    ($#m2_finseq_1 :::"Matrix":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "j1")) "," (Set (Var "j2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i1")) "," (Set (Var "j1")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set (Var "G")))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i2")) "," (Set (Var "j2")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set (Var "G")))) & (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i1")) "," (Set (Var "j1")) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i2")) "," (Set (Var "j2")) ")"  ")" )  ($#k17_euclid :::"`1"::: )  ))) "holds"  (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set (Var "i2"))))) ; 
 
theorem :: JORDAN1G:8 (Bool  "for" (Set (Var "f")) "being"  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )    ($#v1_topreal1 :::"special"::: )     ($#v2_topreal1 :::"unfolded"::: )     ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool  "("  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"<>"::: )  (Set   ($#k20_pscomp_1 :::"N-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k20_pscomp_1 :::"N-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )))  ")" ) "or" (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"<>"::: )  (Set   ($#k21_pscomp_1 :::"N-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k21_pscomp_1 :::"N-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )))  ")" )  ")" )) "holds"  (Bool (Set (Set  "("  ($#k20_pscomp_1 :::"N-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "("  ($#k21_pscomp_1 :::"N-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ) ")" )  ($#k17_euclid :::"`1"::: )  ))) ; 
 
theorem :: JORDAN1G:9 (Bool  "for" (Set (Var "f")) "being"  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )    ($#v1_topreal1 :::"special"::: )     ($#v2_topreal1 :::"unfolded"::: )     ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool  "("  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"<>"::: )  (Set   ($#k20_pscomp_1 :::"N-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k20_pscomp_1 :::"N-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )))  ")" ) "or" (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"<>"::: )  (Set   ($#k21_pscomp_1 :::"N-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k21_pscomp_1 :::"N-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )))  ")" )  ")" )) "holds"  (Bool (Set   ($#k20_pscomp_1 :::"N-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k21_pscomp_1 :::"N-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )))) ; 
 
theorem :: JORDAN1G:10 (Bool  "for" (Set (Var "f")) "being"  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )    ($#v1_topreal1 :::"special"::: )     ($#v2_topreal1 :::"unfolded"::: )     ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool  "("  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"<>"::: )  (Set   ($#k25_pscomp_1 :::"S-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k25_pscomp_1 :::"S-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )))  ")" ) "or" (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"<>"::: )  (Set   ($#k24_pscomp_1 :::"S-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k24_pscomp_1 :::"S-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )))  ")" )  ")" )) "holds"  (Bool (Set (Set  "("  ($#k25_pscomp_1 :::"S-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "("  ($#k24_pscomp_1 :::"S-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ) ")" )  ($#k17_euclid :::"`1"::: )  ))) ; 
 
theorem :: JORDAN1G:11 (Bool  "for" (Set (Var "f")) "being"  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )    ($#v1_topreal1 :::"special"::: )     ($#v2_topreal1 :::"unfolded"::: )     ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool  "("  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"<>"::: )  (Set   ($#k25_pscomp_1 :::"S-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k25_pscomp_1 :::"S-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )))  ")" ) "or" (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"<>"::: )  (Set   ($#k24_pscomp_1 :::"S-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k24_pscomp_1 :::"S-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )))  ")" )  ")" )) "holds"  (Bool (Set   ($#k25_pscomp_1 :::"S-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k24_pscomp_1 :::"S-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )))) ; 
 
theorem :: JORDAN1G:12 (Bool  "for" (Set (Var "f")) "being"  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )    ($#v1_topreal1 :::"special"::: )     ($#v2_topreal1 :::"unfolded"::: )     ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool  "("  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"<>"::: )  (Set   ($#k18_pscomp_1 :::"W-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k18_pscomp_1 :::"W-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )))  ")" ) "or" (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"<>"::: )  (Set   ($#k19_pscomp_1 :::"W-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k19_pscomp_1 :::"W-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )))  ")" )  ")" )) "holds"  (Bool (Set (Set  "("  ($#k18_pscomp_1 :::"W-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ) ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "("  ($#k19_pscomp_1 :::"W-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ) ")" )  ($#k18_euclid :::"`2"::: )  ))) ; 
 
theorem :: JORDAN1G:13 (Bool  "for" (Set (Var "f")) "being"  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )    ($#v1_topreal1 :::"special"::: )     ($#v2_topreal1 :::"unfolded"::: )     ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool  "("  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"<>"::: )  (Set   ($#k18_pscomp_1 :::"W-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k18_pscomp_1 :::"W-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )))  ")" ) "or" (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"<>"::: )  (Set   ($#k19_pscomp_1 :::"W-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k19_pscomp_1 :::"W-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )))  ")" )  ")" )) "holds"  (Bool (Set   ($#k18_pscomp_1 :::"W-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k19_pscomp_1 :::"W-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )))) ; 
 
theorem :: JORDAN1G:14 (Bool  "for" (Set (Var "f")) "being"  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )    ($#v1_topreal1 :::"special"::: )     ($#v2_topreal1 :::"unfolded"::: )     ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool  "("  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"<>"::: )  (Set   ($#k23_pscomp_1 :::"E-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k23_pscomp_1 :::"E-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )))  ")" ) "or" (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"<>"::: )  (Set   ($#k22_pscomp_1 :::"E-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k22_pscomp_1 :::"E-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )))  ")" )  ")" )) "holds"  (Bool (Set (Set  "("  ($#k23_pscomp_1 :::"E-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ) ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "("  ($#k22_pscomp_1 :::"E-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ) ")" )  ($#k18_euclid :::"`2"::: )  ))) ; 
 
theorem :: JORDAN1G:15 (Bool  "for" (Set (Var "f")) "being"  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )    ($#v1_topreal1 :::"special"::: )     ($#v2_topreal1 :::"unfolded"::: )     ($#v2_goboard5 :::"standard"::: )    ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool  "("  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"<>"::: )  (Set   ($#k23_pscomp_1 :::"E-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k23_pscomp_1 :::"E-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )))  ")" ) "or" (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"<>"::: )  (Set   ($#k22_pscomp_1 :::"E-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k22_pscomp_1 :::"E-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )))  ")" )  ")" )) "holds"  (Bool (Set   ($#k23_pscomp_1 :::"E-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k22_pscomp_1 :::"E-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set (Var "f")) ")" )))) ; 
 
theorem :: JORDAN1G:16 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "D"))  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))) & (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "q"))  ($#k4_finseq_4 :::".."::: )  (Set (Var "f")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k4_finseq_4 :::".."::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k1_finseq_5 :::"-:"::: )  (Set (Var "p")) ")" )  ($#k2_finseq_5 :::":-"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k2_finseq_5 :::":-"::: )  (Set (Var "q")) ")" )  ($#k1_finseq_5 :::"-:"::: )  (Set (Var "p"))))))) ; 
 
theorem :: JORDAN1G:17 (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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) ")" )  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "(" (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k1_finseq_5 :::"-:"::: )  (Set  "("  ($#k18_pscomp_1 :::"W-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) ")" ) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "(" (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k2_finseq_5 :::":-"::: )  (Set  "("  ($#k18_pscomp_1 :::"W-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  "("  ($#k20_pscomp_1 :::"N-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) "," (Set  "("  ($#k18_pscomp_1 :::"W-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) ($#k2_tarski :::"}"::: ) )))) ; 
 
theorem :: JORDAN1G:18 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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   ($#k2_jordan1e :::"Lower_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_finseq_6 :::"Rotate"::: )   "(" (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) "," (Set  "("  ($#k22_pscomp_1 :::"E-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) ")"  ")" )  ($#k1_finseq_5 :::"-:"::: )  (Set  "("  ($#k18_pscomp_1 :::"W-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ))))) ; 
 
theorem :: JORDAN1G:19 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#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 (Set  "("  ($#k18_pscomp_1 :::"W-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k4_finseq_4 :::".."::: )  (Set  "("  ($#k1_jordan1e :::"Upper_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Num 1)))) ; 
 
theorem :: JORDAN1G:20 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#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 (Set  "("  ($#k18_pscomp_1 :::"W-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k4_finseq_4 :::".."::: )  (Set  "("  ($#k1_jordan1e :::"Upper_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "("  ($#k19_pscomp_1 :::"W-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k4_finseq_4 :::".."::: )  (Set  "("  ($#k1_jordan1e :::"Upper_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))) ; 
 
theorem :: JORDAN1G:21 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#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 (Set  "("  ($#k19_pscomp_1 :::"W-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k4_finseq_4 :::".."::: )  (Set  "("  ($#k1_jordan1e :::"Upper_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k20_pscomp_1 :::"N-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k4_finseq_4 :::".."::: )  (Set  "("  ($#k1_jordan1e :::"Upper_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))) ; 
 
theorem :: JORDAN1G:22 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#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 (Set  "("  ($#k20_pscomp_1 :::"N-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k4_finseq_4 :::".."::: )  (Set  "("  ($#k1_jordan1e :::"Upper_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "("  ($#k21_pscomp_1 :::"N-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k4_finseq_4 :::".."::: )  (Set  "("  ($#k1_jordan1e :::"Upper_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))) ; 
 
theorem :: JORDAN1G:23 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#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 (Set  "("  ($#k21_pscomp_1 :::"N-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k4_finseq_4 :::".."::: )  (Set  "("  ($#k1_jordan1e :::"Upper_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k22_pscomp_1 :::"E-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k4_finseq_4 :::".."::: )  (Set  "("  ($#k1_jordan1e :::"Upper_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))) ; 
 
theorem :: JORDAN1G:24 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#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 (Set  "("  ($#k22_pscomp_1 :::"E-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k4_finseq_4 :::".."::: )  (Set  "("  ($#k1_jordan1e :::"Upper_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k1_jordan1e :::"Upper_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))) ; 
 
theorem :: JORDAN1G:25 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#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 (Set  "("  ($#k22_pscomp_1 :::"E-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k4_finseq_4 :::".."::: )  (Set  "("  ($#k2_jordan1e :::"Lower_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Num 1)))) ; 
 
theorem :: JORDAN1G:26 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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 (Set  "("  ($#k22_pscomp_1 :::"E-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k4_finseq_4 :::".."::: )  (Set  "("  ($#k2_jordan1e :::"Lower_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "("  ($#k23_pscomp_1 :::"E-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k4_finseq_4 :::".."::: )  (Set  "("  ($#k2_jordan1e :::"Lower_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))) ; 
 
theorem :: JORDAN1G:27 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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 (Set  "("  ($#k23_pscomp_1 :::"E-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k4_finseq_4 :::".."::: )  (Set  "("  ($#k2_jordan1e :::"Lower_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k24_pscomp_1 :::"S-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k4_finseq_4 :::".."::: )  (Set  "("  ($#k2_jordan1e :::"Lower_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))) ; 
 
theorem :: JORDAN1G:28 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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 (Set  "("  ($#k24_pscomp_1 :::"S-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k4_finseq_4 :::".."::: )  (Set  "("  ($#k2_jordan1e :::"Lower_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "("  ($#k25_pscomp_1 :::"S-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k4_finseq_4 :::".."::: )  (Set  "("  ($#k2_jordan1e :::"Lower_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))) ; 
 
theorem :: JORDAN1G:29 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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 (Set  "("  ($#k25_pscomp_1 :::"S-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k4_finseq_4 :::".."::: )  (Set  "("  ($#k2_jordan1e :::"Lower_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k18_pscomp_1 :::"W-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k4_finseq_4 :::".."::: )  (Set  "("  ($#k2_jordan1e :::"Lower_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))) ; 
 
theorem :: JORDAN1G:30 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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 (Set  "("  ($#k18_pscomp_1 :::"W-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k4_finseq_4 :::".."::: )  (Set  "("  ($#k2_jordan1e :::"Lower_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k2_jordan1e :::"Lower_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))) ; 
 
theorem :: JORDAN1G:31 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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 (Set  "(" (Set  "("  ($#k1_jordan1e :::"Upper_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Num 2) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k6_pscomp_1 :::"W-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ))))) ; 
 
theorem :: JORDAN1G:32 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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 (Set  "(" (Set  "("  ($#k2_jordan1e :::"Lower_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Num 2) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k8_pscomp_1 :::"E-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ))))) ; 
 
theorem :: JORDAN1G:33 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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 (Set  "("  ($#k6_pscomp_1 :::"W-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_pscomp_1 :::"E-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_pscomp_1 :::"W-bound"::: )  (Set (Var "C")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_pscomp_1 :::"E-bound"::: )  (Set (Var "C")) ")" ))))) ; 
 
theorem :: JORDAN1G:34 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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 (Set  "("  ($#k9_pscomp_1 :::"S-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k7_pscomp_1 :::"N-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k9_pscomp_1 :::"S-bound"::: )  (Set (Var "C")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k7_pscomp_1 :::"N-bound"::: )  (Set (Var "C")) ")" ))))) ; 
 
theorem :: JORDAN1G:35 (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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) ")" )  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "("  ($#k1_jordan1a :::"Center"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) "," (Set (Var "i")) ")"  ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k6_pscomp_1 :::"W-bound"::: )  (Set (Var "C")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_pscomp_1 :::"E-bound"::: )  (Set (Var "C")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2)))))) ; 
 
theorem :: JORDAN1G:36 (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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) ")" )  (Bool  "for" (Set (Var "n")) "," (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set  "("  ($#k1_jordan1a :::"Center"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")"  ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k9_pscomp_1 :::"S-bound"::: )  (Set (Var "C")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k7_pscomp_1 :::"N-bound"::: )  (Set (Var "C")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2))))) ; 
 
theorem :: JORDAN1G:37 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"S-Sequence_in_R2":::)  (Bool  "for" (Set (Var "k1")) "," (Set (Var "k2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k1"))) & (Bool (Set (Var "k1"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k2"))) & (Bool (Set (Var "k2"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f")) "," (Set (Var "k1")) "," (Set (Var "k2")) ")"  ")" ))) & (Bool (Bool  "not" (Set (Var "k1"))  ($#r1_hidden :::"="::: )  (Num 1)))) "holds"  (Bool (Set (Var "k2"))  ($#r1_hidden :::"="::: )  (Num 1)))) ; 
 
theorem :: JORDAN1G:38 (Bool  "for" (Set (Var "f")) "being"   ($#m2_finseq_1 :::"S-Sequence_in_R2":::)  (Bool  "for" (Set (Var "k1")) "," (Set (Var "k2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k1"))) & (Bool (Set (Var "k1"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k2"))) & (Bool (Set (Var "k2"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f")) "," (Set (Var "k1")) "," (Set (Var "k2")) ")"  ")" ))) & (Bool (Bool  "not" (Set (Var "k1"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))))) "holds"  (Bool (Set (Var "k2"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))))) ; 
 
theorem :: JORDAN1G:39 (Bool  "for" (Set (Var "C")) "being"   ($#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) ")" )  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k1_jordan1e :::"Upper_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k2_jordan1e :::"Lower_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )))  ")" ))) ; 
 
theorem :: JORDAN1G:40 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#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   ($#k1_jordan1e :::"Upper_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")" )  ($#r2_sprect_2 :::"is_a_h.c._for"::: )  (Set   ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")" )))) ; 
 
theorem :: JORDAN1G:41 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#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   ($#k4_finseq_5 :::"Rev"::: )  (Set  "("  ($#k2_jordan1e :::"Lower_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))  ($#r2_sprect_2 :::"is_a_h.c._for"::: )  (Set   ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")" )))) ; 
 
theorem :: JORDAN1G:42 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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) ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )))) "holds"  (Bool  "not" (Bool (Set (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Num 1) ")" )  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k1_jordan1e :::"Upper_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))))) ; 
 
theorem :: JORDAN1G:43 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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) ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )))) "holds"  (Bool  "not" (Bool (Set (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k2_jordan1e :::"Lower_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))))) ; 
 
theorem :: JORDAN1G:44 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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) ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )))) "holds"  (Bool  "not" (Bool (Set (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Num 1) ")" )  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan1e :::"Upper_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))))) ; 
 
theorem :: JORDAN1G:45 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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) ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )))) "holds"  (Bool  "not" (Bool (Set (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set  "("  ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k2_jordan1e :::"Lower_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))))) ; 
 
theorem :: JORDAN1G:46 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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) ")" )  (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))) & (Bool (Set (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )))) "holds"  (Bool (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set  "(" (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Num 1) ")"  ")" ) "," (Set  "(" (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")"  ")" ) ")" )  ($#r1_xboole_0 :::"meets"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k2_jordan1e :::"Lower_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )))))) ; 
 
theorem :: JORDAN1G:47 (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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) ")" )  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k1_jordan5c :::"First_Point"::: )   "(" (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan1e :::"Upper_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) "," (Set  "("  ($#k18_pscomp_1 :::"W-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) "," (Set  "("  ($#k22_pscomp_1 :::"E-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) "," (Set  "("  ($#k6_jordan6 :::"Vertical_Line"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k6_pscomp_1 :::"W-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_pscomp_1 :::"E-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k1_jordan1e :::"Upper_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))) ; 
 
theorem :: JORDAN1G:48 (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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) ")" )  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k2_jordan5c :::"Last_Point"::: )   "(" (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k2_jordan1e :::"Lower_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) "," (Set  "("  ($#k22_pscomp_1 :::"E-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) "," (Set  "("  ($#k18_pscomp_1 :::"W-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) "," (Set  "("  ($#k6_jordan6 :::"Vertical_Line"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k6_pscomp_1 :::"W-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_pscomp_1 :::"E-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k2_jordan1e :::"Lower_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))))) ; 
 
theorem :: JORDAN1G:49 (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) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k3_jordan3 :::"R_Cut"::: )   "(" (Set (Var "f")) "," (Set (Var "p")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f")) "," (Num 1) "," (Set  "(" (Set (Var "p"))  ($#k4_finseq_4 :::".."::: )  (Set (Var "f")) ")" ) ")" )))) ; 
 
theorem :: JORDAN1G:50 (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")))) & (Bool (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")) ")" )  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set (Var "f")) "," (Num 1) "," (Set  "(" (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")) ")"  ")" )  ($#k4_finseq_4 :::".."::: )  (Set (Var "f")) ")" ) ")"  ")" ) ")" )  ($#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 :: JORDAN1G:51 (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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) ")" )  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "("  ($#k1_jordan5c :::"First_Point"::: )   "(" (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan1e :::"Upper_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) "," (Set  "("  ($#k18_pscomp_1 :::"W-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) "," (Set  "("  ($#k22_pscomp_1 :::"E-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) "," (Set  "("  ($#k6_jordan6 :::"Vertical_Line"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k6_pscomp_1 :::"W-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_pscomp_1 :::"E-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" ) ")" ) ")"  ")" )  ($#k4_finseq_4 :::".."::: )  (Set  "("  ($#k1_jordan1e :::"Upper_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k1_jordan1e :::"Upper_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "k")) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set  "("  ($#k6_pscomp_1 :::"W-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_pscomp_1 :::"E-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2)))))) ; 
 
theorem :: JORDAN1G:52 (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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) ")" )  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "("  ($#k1_jordan5c :::"First_Point"::: )   "(" (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k4_finseq_5 :::"Rev"::: )  (Set  "("  ($#k2_jordan1e :::"Lower_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) "," (Set  "("  ($#k18_pscomp_1 :::"W-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) "," (Set  "("  ($#k22_pscomp_1 :::"E-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) "," (Set  "("  ($#k6_jordan6 :::"Vertical_Line"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k6_pscomp_1 :::"W-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_pscomp_1 :::"E-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" ) ")" ) ")"  ")" )  ($#k4_finseq_4 :::".."::: )  (Set  "("  ($#k4_finseq_5 :::"Rev"::: )  (Set  "("  ($#k2_jordan1e :::"Lower_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" )))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k4_finseq_5 :::"Rev"::: )  (Set  "("  ($#k2_jordan1e :::"Lower_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "k")) ")" )  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set  "(" (Set  "("  ($#k6_pscomp_1 :::"W-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_pscomp_1 :::"E-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2)))))) ; 
 
theorem :: JORDAN1G:53 (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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) ")" )  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k3_finseq_6 :::"mid"::: )   "(" (Set  "("  ($#k1_jordan1e :::"Upper_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) "," (Num 2) "," (Set  "(" (Set  "("  ($#k1_jordan5c :::"First_Point"::: )   "(" (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan1e :::"Upper_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) "," (Set  "("  ($#k18_pscomp_1 :::"W-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) "," (Set  "("  ($#k22_pscomp_1 :::"E-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) "," (Set  "("  ($#k6_jordan6 :::"Vertical_Line"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k6_pscomp_1 :::"W-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_pscomp_1 :::"E-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" ) ")" ) ")"  ")" )  ($#k4_finseq_4 :::".."::: )  (Set  "("  ($#k1_jordan1e :::"Upper_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")"  ")" )))) "holds"  (Bool (Set (Set (Var "q"))  ($#k17_euclid :::"`1"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "("  ($#k6_pscomp_1 :::"W-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_pscomp_1 :::"E-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2)))))) ; 
 
theorem :: JORDAN1G:54 (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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) ")" )  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k1_jordan5c :::"First_Point"::: )   "(" (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan1e :::"Upper_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) "," (Set  "("  ($#k18_pscomp_1 :::"W-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) "," (Set  "("  ($#k22_pscomp_1 :::"E-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) "," (Set  "("  ($#k6_jordan6 :::"Vertical_Line"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k6_pscomp_1 :::"W-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_pscomp_1 :::"E-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" ) ")" ) ")"  ")" )  ($#k18_euclid :::"`2"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set (Set  "("  ($#k2_jordan5c :::"Last_Point"::: )   "(" (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k2_jordan1e :::"Lower_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) "," (Set  "("  ($#k22_pscomp_1 :::"E-max"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) "," (Set  "("  ($#k18_pscomp_1 :::"W-min"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) "," (Set  "("  ($#k6_jordan6 :::"Vertical_Line"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k6_pscomp_1 :::"W-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_pscomp_1 :::"E-bound"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" ) ")" ) ")"  ")" )  ($#k18_euclid :::"`2"::: )  )))) ; 
 
theorem :: JORDAN1G:55 (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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) ")" )  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan1e :::"Upper_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k8_jordan6 :::"Upper_Arc"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ))))) ; 
 
theorem :: JORDAN1G:56 (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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) ")" )  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k2_jordan1e :::"Lower_Seq"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k9_jordan6 :::"Lower_Arc"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" ))))) ; 
 
theorem :: JORDAN1G:57 (Bool  "for" (Set (Var "C")) "being"   ($#v2_connsp_1 :::"connected"::: )     ($#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) ")" )  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_matrix_1 :::"width"::: )  (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ))) & (Bool (Set (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r2_hidden :::"in"::: )  (Set   ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )))) "holds"  (Bool (Set   ($#k1_rltopsp1 :::"LSeg"::: )   "(" (Set  "(" (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Num 1) ")"  ")" ) "," (Set  "(" (Set  "("  ($#k1_jordan8 :::"Gauge"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")"  ")" ) ")" )  ($#r1_xboole_0 :::"meets"::: )  (Set   ($#k9_jordan6 :::"Lower_Arc"::: )  (Set  "("  ($#k3_topreal1 :::"L~"::: )  (Set  "("  ($#k1_jordan9 :::"Cage"::: )   "(" (Set (Var "C")) "," (Set (Var "n")) ")"  ")" ) ")" )))))) ;