:: SIMPLEX2  semantic presentation begin  






definitionlet "M" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::); assume 
(Bool (Set   ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Const "M"))) "is"   ($#v1_compts_1 :::"compact"::: )  )
 ; let "F" be   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Const "M")) ")" ); assume that  
(Bool (Set (Const "F")) "is"   ($#v1_tops_2 :::"open"::: )  )
 and  
(Bool (Set (Const "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Const "M")) ")" ))
 ; mode  :::"Lebesgue_number":::  "of" "F" ->   ($#v2_xxreal_0 :::"positive"::: )    ($#m1_subset_1 :::"Real":::) means :: SIMPLEX2:def 1 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" "M" (Bool  "ex" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  "M" ")" ) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  "F") & (Bool (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "p")) "," it ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "A")))  ")" ))); end; 







:: deftheorem    defines :::"Lebesgue_number"::: SIMPLEX2:def 1 :  (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::)  "st" (Bool (Bool (Set   ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "M"))) "is"   ($#v1_compts_1 :::"compact"::: )  )) "holds"  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "M")) ")" )  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "M")) ")" ))) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#v2_xxreal_0 :::"positive"::: )    ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Var "b3")) "is"    ($#m1_simplex2 :::"Lebesgue_number"::: )   "of" (Set (Var "F"))) "iff" (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool  "ex" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "M")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "F"))) & (Bool (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "p")) "," (Set (Var "b3")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "A")))  ")" )))  ")" )))); 
 



theorem :: SIMPLEX2:1 (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::)  (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"   ($#v1_tops_2 :::"open"::: )    ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "M")) ")" )  (Bool  "for" (Set (Var "L")) "being"    ($#m1_simplex2 :::"Lebesgue_number"::: )   "of" (Set (Var "F"))  "st" (Bool (Bool (Set   ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "M"))) "is"   ($#v1_compts_1 :::"compact"::: )  ) & (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "M")) ")" )) & (Bool (Set (Var "F"))  ($#r1_tarski :::"c="::: )  (Set (Var "G")))) "holds"  (Bool (Set (Var "L")) "is"    ($#m1_simplex2 :::"Lebesgue_number"::: )   "of" (Set (Var "G")))))) ; 
 
theorem :: SIMPLEX2:2 (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::)  (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"   ($#v1_tops_2 :::"open"::: )    ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "M")) ")" )  (Bool  "for" (Set (Var "L")) "being"    ($#m1_simplex2 :::"Lebesgue_number"::: )   "of" (Set (Var "F"))  "st" (Bool (Bool (Set   ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "M"))) "is"   ($#v1_compts_1 :::"compact"::: )  ) & (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "M")) ")" )) & (Bool (Set (Var "F"))  ($#r1_setfam_1 :::"is_finer_than"::: )  (Set (Var "G")))) "holds"  (Bool (Set (Var "L")) "is"    ($#m1_simplex2 :::"Lebesgue_number"::: )   "of" (Set (Var "G")))))) ; 
 
theorem :: SIMPLEX2:3 (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::)  (Bool  "for" (Set (Var "F")) "being"   ($#v1_tops_2 :::"open"::: )    ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "M")) ")" )  (Bool  "for" (Set (Var "L")) "being"    ($#m1_simplex2 :::"Lebesgue_number"::: )   "of" (Set (Var "F"))  (Bool  "for" (Set (Var "L1")) "being"   ($#v2_xxreal_0 :::"positive"::: )    ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "M"))) "is"   ($#v1_compts_1 :::"compact"::: )  ) & (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "M")) ")" )) & (Bool (Set (Var "L1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "L")))) "holds"  (Bool (Set (Var "L1")) "is"    ($#m1_simplex2 :::"Lebesgue_number"::: )   "of" (Set (Var "F"))))))) ; 
 begin  


















registrationlet "M" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#l1_metric_1 :::"MetrStruct"::: )  ; 
cluster   ($#v1_finset_1 :::"finite"::: )    ->   ($#v6_tbsp_1 :::"bounded"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "M")); 
end; 
theorem :: SIMPLEX2:4 (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "S")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool  "ex" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "S"))) & (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Var "S"))) & (Bool (Set   ($#k2_metric_1 :::"dist"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_tbsp_1 :::"diameter"::: )  (Set (Var "S"))))  ")" )))) ; 
 definitionlet "M" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#l1_metric_1 :::"MetrStruct"::: )  ; let "K" be   ($#l1_pre_topc :::"SimplicialComplexStr":::); attr "K" is "M" :::"bounded":::  means :: SIMPLEX2:def 2 (Bool  "ex" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "M"  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" "K"))) "holds"  (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v6_tbsp_1 :::"bounded"::: )  ) & (Bool (Set   ($#k3_tbsp_1 :::"diameter"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))  ")" ))); end; 





:: deftheorem    defines :::"bounded"::: SIMPLEX2:def 2 :  (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "K")) "being"   ($#l1_pre_topc :::"SimplicialComplexStr":::) "holds"   (Bool  "("  (Bool (Set (Var "K")) "is" (Set (Var "M"))  ($#v1_simplex2 :::"bounded"::: )  ) "iff" (Bool  "ex" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M"))  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "K"))))) "holds"  (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v6_tbsp_1 :::"bounded"::: )  ) & (Bool (Set   ($#k3_tbsp_1 :::"diameter"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))  ")" )))  ")" ))); 
 
theorem :: SIMPLEX2:5 (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M"))  (Bool  "for" (Set (Var "K")) "being"  ($#~v3_pencil_1  "non"   ($#v3_pencil_1 :::"void"::: )   )   ($#l1_pre_topc :::"SimplicialComplexStr":::)  "st" (Bool (Bool (Set (Var "K")) "is" (Set (Var "M"))  ($#v1_simplex2 :::"bounded"::: )  ) & (Bool (Set (Var "A")) "is"   ($#m1_subset_1 :::"Simplex":::) "of" (Set (Var "K")))) "holds"  (Bool (Set (Var "A")) "is"   ($#v6_tbsp_1 :::"bounded"::: )  )))) ; 
 registrationlet "M" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#l1_metric_1 :::"MetrStruct"::: )  ; let "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster  ($#~v3_pencil_1  "non"   ($#v3_pencil_1 :::"void"::: )   )    ($#v1_matroid0 :::"subset-closed"::: )     ($#v3_matroid0 :::"finite-membered"::: )   "M"  ($#v1_simplex2 :::"bounded"::: )    for    ($#m1_simplex0 :::"SimplicialComplexStr"::: )   "of" "X"; 
end; registrationlet "M" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#l1_metric_1 :::"MetrStruct"::: )  ; 
cluster  ($#~v3_pencil_1  "non"   ($#v3_pencil_1 :::"void"::: )   )    ($#v1_matroid0 :::"subset-closed"::: )     ($#v3_matroid0 :::"finite-membered"::: )   "M"  ($#v1_simplex2 :::"bounded"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; registrationlet "M" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#l1_metric_1 :::"MetrStruct"::: )  ; let "X" be    ($#m1_hidden :::"set"::: )  ; let "K" be (Set (Const "M"))  ($#v1_simplex2 :::"bounded"::: )     ($#m1_simplex0 :::"SimplicialComplexStr"::: )   "of" (Set (Const "X")); 
cluster   -> "M"  ($#v1_simplex2 :::"bounded"::: )    for    ($#m2_simplex0 :::"SubSimplicialComplex"::: )   "of" "K"; 
end; registrationlet "M" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#l1_metric_1 :::"MetrStruct"::: )  ; let "X" be    ($#m1_hidden :::"set"::: )  ; let "K" be   ($#v1_matroid0 :::"subset-closed"::: )   (Set (Const "M"))  ($#v1_simplex2 :::"bounded"::: )     ($#m1_simplex0 :::"SimplicialComplexStr"::: )   "of" (Set (Const "X")); let "i" be   ($#m1_hidden :::"Integer":::); 
cluster (Set   ($#k8_simplex0 :::"Skeleton_of"::: )   "(" "K" "," "i" ")" ) -> "M"  ($#v1_simplex2 :::"bounded"::: )   ; 
end; 
theorem :: SIMPLEX2:6 (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "K")) "being"   ($#l1_pre_topc :::"SimplicialComplexStr":::)  "st" (Bool (Bool (Set (Var "K")) "is"   ($#v2_simplex0 :::"finite-vertices"::: )  )) "holds"  (Bool (Set (Var "K")) "is" (Set (Var "M"))  ($#v1_simplex2 :::"bounded"::: )  ))) ; 
 begin  definitionlet "M" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#l1_metric_1 :::"MetrStruct"::: )  ; let "K" be   ($#l1_pre_topc :::"SimplicialComplexStr":::); assume 
(Bool (Set (Const "K")) "is" (Set (Const "M"))  ($#v1_simplex2 :::"bounded"::: )  )
 ; func  :::"diameter":::  "(" "M" "," "K" ")"  ->   ($#m1_subset_1 :::"Real":::) means :: SIMPLEX2:def 3 (Bool  "("  (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "M"  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" "K"))) "holds"  (Bool (Set   ($#k3_tbsp_1 :::"diameter"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::"<="::: )  it)  ")" ) & (Bool  "("   "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "M"  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" "K"))) "holds"  (Bool (Set   ($#k3_tbsp_1 :::"diameter"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))  ")" )) "holds"  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">="::: )  it)  ")" )  ")" ) if (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" "K")  ($#r1_xboole_0 :::"meets"::: )  (Set   ($#k9_setfam_1 :::"bool"::: )  (Set  "("  ($#k2_struct_0 :::"[#]"::: )  "M" ")" )))  otherwise (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"0"::: )  )); end; 







:: deftheorem    defines :::"diameter"::: SIMPLEX2:def 3 :  (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "K")) "being"   ($#l1_pre_topc :::"SimplicialComplexStr":::)  "st" (Bool (Bool (Set (Var "K")) "is" (Set (Var "M"))  ($#v1_simplex2 :::"bounded"::: )  )) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "K")))  ($#r1_xboole_0 :::"meets"::: )  (Set   ($#k9_setfam_1 :::"bool"::: )  (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "M")) ")" )))) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_simplex2 :::"diameter"::: )   "(" (Set (Var "M")) "," (Set (Var "K")) ")" )) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M"))  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "K"))))) "holds"  (Bool (Set   ($#k3_tbsp_1 :::"diameter"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b3")))  ")" ) & (Bool  "("   "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M"))  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "K"))))) "holds"  (Bool (Set   ($#k3_tbsp_1 :::"diameter"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))  ")" )) "holds"  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "b3")))  ")" )  ")" )  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "K")))  ($#r1_xboole_0 :::"meets"::: )  (Set   ($#k9_setfam_1 :::"bool"::: )  (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "M")) ")" ))))) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_simplex2 :::"diameter"::: )   "(" (Set (Var "M")) "," (Set (Var "K")) ")" )) "iff" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"0"::: )  ))  ")" )  ")"   ")" )))); 
 
theorem :: SIMPLEX2:7 (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "K")) "being"   ($#l1_pre_topc :::"SimplicialComplexStr":::)  "st" (Bool (Bool (Set (Var "K")) "is" (Set (Var "M"))  ($#v1_simplex2 :::"bounded"::: )  )) "holds"  (Bool (Set   ($#k1_xboole_0 :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_simplex2 :::"diameter"::: )   "(" (Set (Var "M")) "," (Set (Var "K")) ")" )))) ; 
 
theorem :: SIMPLEX2:8 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "K")) "being" (Set (Var "b2"))  ($#v1_simplex2 :::"bounded"::: )     ($#m1_simplex0 :::"SimplicialComplexStr"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "KX")) "being"    ($#m2_simplex0 :::"SubSimplicialComplex"::: )   "of" (Set (Var "K")) "holds"  (Bool (Set   ($#k1_simplex2 :::"diameter"::: )   "(" (Set (Var "M")) "," (Set (Var "KX")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_simplex2 :::"diameter"::: )   "(" (Set (Var "M")) "," (Set (Var "K")) ")" )))))) ; 
 
theorem :: SIMPLEX2:9 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "K")) "being"   ($#v1_matroid0 :::"subset-closed"::: )   (Set (Var "b2"))  ($#v1_simplex2 :::"bounded"::: )     ($#m1_simplex0 :::"SimplicialComplexStr"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set   ($#k1_simplex2 :::"diameter"::: )   "(" (Set (Var "M")) "," (Set  "("  ($#k9_simplex0 :::"Skeleton_of"::: )   "(" (Set (Var "K")) "," (Set (Var "i")) ")"  ")" ) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_simplex2 :::"diameter"::: )   "(" (Set (Var "M")) "," (Set (Var "K")) ")" )))))) ; 
 definitionlet "M" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#l1_metric_1 :::"MetrStruct"::: )  ; let "K" be  ($#~v3_pencil_1  "non"   ($#v3_pencil_1 :::"void"::: )   )    ($#v1_matroid0 :::"subset-closed"::: )   (Set (Const "M"))  ($#v1_simplex2 :::"bounded"::: )    ($#l1_pre_topc :::"SimplicialComplexStr":::); :: original: :::"diameter"::: redefine func  :::"diameter":::  "(" "M" "," "K" ")"  ->   ($#m1_subset_1 :::"Real":::) means :: SIMPLEX2:def 4 (Bool  "("  (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "M"  "st" (Bool (Bool (Set (Var "A")) "is"   ($#m1_subset_1 :::"Simplex":::) "of" "K")) "holds"  (Bool (Set   ($#k3_tbsp_1 :::"diameter"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::"<="::: )  it)  ")" ) & (Bool  "("   "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "M"  "st" (Bool (Bool (Set (Var "A")) "is"   ($#m1_subset_1 :::"Simplex":::) "of" "K")) "holds"  (Bool (Set   ($#k3_tbsp_1 :::"diameter"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))  ")" )) "holds"  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">="::: )  it)  ")" )  ")" ); end; 






:: deftheorem    defines :::"diameter"::: SIMPLEX2:def 4 :  (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "K")) "being"  ($#~v3_pencil_1  "non"   ($#v3_pencil_1 :::"void"::: )   )    ($#v1_matroid0 :::"subset-closed"::: )   (Set (Var "b1"))  ($#v1_simplex2 :::"bounded"::: )    ($#l1_pre_topc :::"SimplicialComplexStr":::)  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_simplex2 :::"diameter"::: )   "(" (Set (Var "M")) "," (Set (Var "K")) ")" )) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#m1_subset_1 :::"Simplex":::) "of" (Set (Var "K")))) "holds"  (Bool (Set   ($#k3_tbsp_1 :::"diameter"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b3")))  ")" ) & (Bool  "("   "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#m1_subset_1 :::"Simplex":::) "of" (Set (Var "K")))) "holds"  (Bool (Set   ($#k3_tbsp_1 :::"diameter"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))  ")" )) "holds"  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "b3")))  ")" )  ")" )  ")" )))); 
 
theorem :: SIMPLEX2:10 (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "S")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "holds"  (Bool (Set   ($#k1_simplex2 :::"diameter"::: )   "(" (Set (Var "M")) "," (Set  "("  ($#k5_simplex0 :::"Complex_of"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "S")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_tbsp_1 :::"diameter"::: )  (Set (Var "S")))))) ; 
 definitionlet "n" be   ($#m1_hidden :::"Nat":::); let "K" be   ($#m1_simplex0 :::"SimplicialComplexStr":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); attr "K" is  :::"bounded":::  means :: SIMPLEX2:def 5 (Bool "K" "is" (Set   ($#k14_euclid :::"Euclid"::: )  "n")  ($#v1_simplex2 :::"bounded"::: )  ); func  :::"diameter"::: "K" ->   ($#m1_subset_1 :::"Real":::) equals :: SIMPLEX2:def 6 (Set   ($#k1_simplex2 :::"diameter"::: )   "(" (Set  "("  ($#k14_euclid :::"Euclid"::: )  "n" ")" ) "," "K" ")" ); end; 











:: deftheorem    defines :::"bounded"::: SIMPLEX2:def 5 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#m1_simplex0 :::"SimplicialComplexStr":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "K")) "is"   ($#v2_simplex2 :::"bounded"::: )  ) "iff" (Bool (Set (Var "K")) "is" (Set   ($#k14_euclid :::"Euclid"::: )  (Set (Var "n")))  ($#v1_simplex2 :::"bounded"::: )  )  ")" ))); 
 
:: deftheorem    defines :::"diameter"::: SIMPLEX2:def 6 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#m1_simplex0 :::"SimplicialComplexStr":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set   ($#k3_simplex2 :::"diameter"::: )  (Set (Var "K")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_simplex2 :::"diameter"::: )   "(" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Set (Var "n")) ")" ) "," (Set (Var "K")) ")" )))); 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster   ($#v2_simplex2 :::"bounded"::: )    -> (Set   ($#k14_euclid :::"Euclid"::: )  "n")  ($#v1_simplex2 :::"bounded"::: )    for    ($#m1_simplex0 :::"SimplicialComplexStr"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" )); 

cluster  ($#~v3_pencil_1  "non"   ($#v3_pencil_1 :::"void"::: )   )    ($#v1_matroid0 :::"subset-closed"::: )     ($#v3_matroid0 :::"finite-membered"::: )     ($#v4_matroid0 :::"finite-degree"::: )     ($#v6_simplex0 :::"total"::: )     ($#v1_simplex1 :::"affinely-independent"::: )     ($#v2_simplex1 :::"simplex-join-closed"::: )     ($#v2_simplex2 :::"bounded"::: )    for    ($#m1_simplex0 :::"SimplicialComplexStr"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" )); 

cluster   ($#v2_simplex0 :::"finite-vertices"::: )    ->   ($#v2_simplex2 :::"bounded"::: )    for    ($#m1_simplex0 :::"SimplicialComplexStr"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" )); 
end; begin  






theorem :: SIMPLEX2:11 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "Kv")) "being"  ($#~v3_pencil_1  "non"   ($#v3_pencil_1 :::"void"::: )   )   ($#m1_simplex0 :::"SimplicialComplex":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"Simplex":::) "of" (Set  "("  ($#k4_simplex1 :::"BCS"::: )  (Set (Var "Kv")) ")" )  (Bool  "for" (Set (Var "F")) "being"   ($#v6_ordinal1 :::"c=-linear"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v5_finset_1 :::"finite-membered"::: )    ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "S"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_rlaffin2 :::"center_of_mass"::: )  (Set (Var "V")) ")" )  ($#k7_relset_1 :::".:"::: )  (Set (Var "F"))))) "holds"  (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "a1"))  ($#r2_hidden :::"in"::: )  (Set (Var "S"))) & (Bool (Set (Var "a2"))  ($#r2_hidden :::"in"::: )  (Set (Var "S")))) "holds"  (Bool  "ex" (Set (Var "b1")) "," (Set (Var "b2")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V"))(Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "b1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_simplex0 :::"Vertices"::: )  (Set  "("  ($#k4_simplex1 :::"BCS"::: )  (Set  "("  ($#k5_simplex0 :::"Complex_of"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k5_setfam_1 :::"union"::: )  (Set (Var "F")) ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ))) & (Bool (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_simplex0 :::"Vertices"::: )  (Set  "("  ($#k4_simplex1 :::"BCS"::: )  (Set  "("  ($#k5_simplex0 :::"Complex_of"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k5_setfam_1 :::"union"::: )  (Set (Var "F")) ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ))) & (Bool (Set (Set (Var "a1"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "a2")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" (Set (Var "b1"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "b2")) ")" ))) & (Bool (Set   ($#k1_xboole_0 :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k5_setfam_1 :::"union"::: )  (Set (Var "F")) ")" ) ")" )  ($#k5_real_1 :::"-"::: )  (Num 1) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k5_setfam_1 :::"union"::: )  (Set (Var "F")) ")" ) ")" )))  ")" )))))))) ; 
 
theorem :: SIMPLEX2:12 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "E")) "being"    ($#m2_rlaffin3 :::"Enumeration"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Bool  "not" (Set (Set  "("  ($#k4_finseq_1 :::"dom"::: )  (Set (Var "E")) ")" )  ($#k7_subset_1 :::"\"::: )  (Set (Var "X"))) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool (Set   ($#k3_convex1 :::"conv"::: )  (Set  "(" (Set (Var "E"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_setfam_1 :::"meet"::: )   "{"  (Set  "("  ($#k3_convex1 :::"conv"::: )  (Set  "(" (Set (Var "A"))  ($#k7_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "(" (Set (Var "E"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")) ")" ) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) where k "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k4_finseq_1 :::"dom"::: )  (Set (Var "E")) ")" )  ($#k7_subset_1 :::"\"::: )  (Set (Var "X"))))  "}"  )))))) ; 
 



theorem :: SIMPLEX2:13 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "a")) "being"   ($#v6_tbsp_1 :::"bounded"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "A")))) "holds"  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_convex1 :::"conv"::: )  (Set (Var "A"))))) "holds"  (Bool (Set   ($#k3_convex1 :::"conv"::: )  (Set (Var "A")))  ($#r1_tarski :::"c="::: )  (Set   ($#k10_metric_1 :::"cl_Ball"::: )   "(" (Set (Var "p")) "," (Set  "("  ($#k3_tbsp_1 :::"diameter"::: )  (Set (Var "a")) ")" ) ")" )))))) ; 
 
theorem :: SIMPLEX2:14 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v9_rltopsp1 :::"bounded"::: )  ) "iff" (Bool (Set   ($#k3_convex1 :::"conv"::: )  (Set (Var "A"))) "is"   ($#v9_rltopsp1 :::"bounded"::: )  )  ")" ))) ; 
 
theorem :: SIMPLEX2:15 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "a")) "," (Set (Var "ca")) "being"   ($#v6_tbsp_1 :::"bounded"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "ca"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_convex1 :::"conv"::: )  (Set (Var "A")))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "A")))) "holds"  (Bool (Set   ($#k3_tbsp_1 :::"diameter"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tbsp_1 :::"diameter"::: )  (Set (Var "ca"))))))) ; 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); let "K" be   ($#v2_simplex2 :::"bounded"::: )    ($#m1_simplex0 :::"SimplicialComplexStr":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); 
cluster   ->   ($#v2_simplex2 :::"bounded"::: )    for    ($#m1_simplex1 :::"SubdivisionStr"::: )   "of" "K"; 
end; 
theorem :: SIMPLEX2:16 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"  ($#~v3_pencil_1  "non"   ($#v3_pencil_1 :::"void"::: )   )    ($#v4_matroid0 :::"finite-degree"::: )     ($#v2_simplex2 :::"bounded"::: )    ($#m1_simplex0 :::"SimplicialComplex":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set  ($#k3_simplex1 :::"|."::: ) (Set (Var "K")) ($#k3_simplex1 :::".|"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "K"))))) "holds"  (Bool (Set   ($#k3_simplex2 :::"diameter"::: )  (Set  "("  ($#k4_simplex1 :::"BCS"::: )  (Set (Var "K")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "("  ($#k6_simplex0 :::"degree"::: )  (Set (Var "K")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set  "("  ($#k6_simplex0 :::"degree"::: )  (Set (Var "K")) ")" )  ($#k3_real_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k4_real_1 :::"*"::: )  (Set  "("  ($#k3_simplex2 :::"diameter"::: )  (Set (Var "K")) ")" ))))) ; 
 
theorem :: SIMPLEX2:17 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"  ($#~v3_pencil_1  "non"   ($#v3_pencil_1 :::"void"::: )   )    ($#v4_matroid0 :::"finite-degree"::: )     ($#v2_simplex2 :::"bounded"::: )    ($#m1_simplex0 :::"SimplicialComplex":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set  ($#k3_simplex1 :::"|."::: ) (Set (Var "K")) ($#k3_simplex1 :::".|"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "K"))))) "holds"  (Bool (Set   ($#k3_simplex2 :::"diameter"::: )  (Set  "("  ($#k5_simplex1 :::"BCS"::: )   "(" (Set (Var "k")) "," (Set (Var "K")) ")"  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k6_simplex0 :::"degree"::: )  (Set (Var "K")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set  "("  ($#k6_simplex0 :::"degree"::: )  (Set (Var "K")) ")" )  ($#k3_real_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k1_newton :::"|^"::: )  (Set (Var "k")) ")" )  ($#k4_real_1 :::"*"::: )  (Set  "("  ($#k3_simplex2 :::"diameter"::: )  (Set (Var "K")) ")" ))))) ; 
 
theorem :: SIMPLEX2:18 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"  ($#~v3_pencil_1  "non"   ($#v3_pencil_1 :::"void"::: )   )    ($#v4_matroid0 :::"finite-degree"::: )     ($#v2_simplex2 :::"bounded"::: )    ($#m1_simplex0 :::"SimplicialComplex":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set  ($#k3_simplex1 :::"|."::: ) (Set (Var "K")) ($#k3_simplex1 :::".|"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "K"))))) "holds"  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k1_xboole_0 :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set   ($#k3_simplex2 :::"diameter"::: )  (Set  "("  ($#k5_simplex1 :::"BCS"::: )   "(" (Set (Var "k")) "," (Set (Var "K")) ")"  ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))))))) ; 
 
theorem :: SIMPLEX2:19 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "i")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "j")) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set  "(" (Set (Var "i"))  ($#k7_real_1 :::"+"::: )  (Set (Var "j")) ")" ) ")" ) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool  "("   "for" (Set (Var "fi")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "i")) ")" )  (Bool  "for" (Set (Var "fj")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "j")) ")" ) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "fi")) "," (Set (Var "fj")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "fi"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "fj")))))  ")" )  ")" ))) ; 
 
theorem :: SIMPLEX2:20 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "i")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "j")) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set  "(" (Set (Var "i"))  ($#k7_real_1 :::"+"::: )  (Set (Var "j")) ")" ) ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "fi")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "i")) ")" )  (Bool  "for" (Set (Var "fj")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "j")) ")" ) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "fi")) "," (Set (Var "fj")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "fi"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "fj")))))  ")" )) "holds"  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "fi")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Set (Var "i")) ")" )  (Bool  "for" (Set (Var "fj")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Set (Var "j")) ")" )  (Bool  "for" (Set (Var "fij")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Set  "(" (Set (Var "i"))  ($#k7_real_1 :::"+"::: )  (Set (Var "j")) ")" ) ")" )  "st" (Bool (Bool (Set (Var "fij"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "fi"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "fj"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  ($#k3_borsuk_1 :::"[:"::: ) (Set  "("  ($#k4_euclid_9 :::"OpenHypercube"::: )   "(" (Set (Var "fi")) "," (Set (Var "r")) ")"  ")" ) "," (Set  "("  ($#k4_euclid_9 :::"OpenHypercube"::: )   "(" (Set (Var "fj")) "," (Set (Var "r")) ")"  ")" ) ($#k3_borsuk_1 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_euclid_9 :::"OpenHypercube"::: )   "(" (Set (Var "fij")) "," (Set (Var "r")) ")" )))))))) ; 
 
theorem :: SIMPLEX2:21 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v9_rltopsp1 :::"bounded"::: )  ) "iff" (Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Set (Var "n")) ")" )(Bool  "ex" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st" (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set   ($#k4_euclid_9 :::"OpenHypercube"::: )   "(" (Set (Var "p")) "," (Set (Var "r")) ")" ))))  ")" ))) ; 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster   ($#v4_pre_topc :::"closed"::: )     ($#v9_rltopsp1 :::"bounded"::: )    ->   ($#v2_compts_1 :::"compact"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ))); 
end; registrationlet "n" be   ($#m1_hidden :::"Nat":::); let "A" be   ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); 
cluster (Set   ($#k3_convex1 :::"conv"::: )  "A") ->   ($#v2_compts_1 :::"compact"::: )   ; 
end; begin  
theorem :: SIMPLEX2:22 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "E")) "being"    ($#m2_rlaffin3 :::"Enumeration"::: )   "of" (Set (Var "A"))  (Bool  "for" (Set (Var "F")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k9_setfam_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k3_convex1 :::"conv"::: )  (Set (Var "A")) ")" ) ")" )))  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "A")))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "F"))) "is"   ($#v2_tops_2 :::"closed"::: )  ) & (Bool  "("   "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_finseq_1 :::"dom"::: )  (Set (Var "F")) ")" ) "holds"  (Bool (Set   ($#k3_convex1 :::"conv"::: )  (Set  "(" (Set (Var "E"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "S")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k5_setfam_1 :::"union"::: )  (Set  "(" (Set (Var "F"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "S")) ")" )))  ")" )) "holds"  (Bool  "not" (Bool (Set   ($#k6_setfam_1 :::"meet"::: )  (Set  "("  ($#k2_relset_1 :::"rng"::: )  (Set (Var "F")) ")" )) "is"   ($#v1_xboole_0 :::"empty"::: )  )))))) ; 
 



theorem :: SIMPLEX2:23 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "A")) "being"   ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k3_real_1 :::"+"::: )  (Num 1)))) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k3_convex1 :::"conv"::: )  (Set (Var "A")) ")" ) ")" ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k3_convex1 :::"conv"::: )  (Set (Var "A")) ")" ) ")" ) (Bool  "ex" (Set (Var "p")) "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_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "p")))  ")" ))))) ; 
 
theorem :: SIMPLEX2:24 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "A")) "being"   ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k3_real_1 :::"+"::: )  (Num 1)))) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k3_convex1 :::"conv"::: )  (Set (Var "A")) ")" ) ")" ) "," (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k3_convex1 :::"conv"::: )  (Set (Var "A")) ")" ) ")" ) "holds"  (Bool (Set (Var "f")) "is"   ($#v2_abian :::"with_fixpoint"::: )  )))) ; 
 
theorem :: SIMPLEX2:25 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "A")) "being"   ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k3_real_1 :::"+"::: )  (Num 1)))) "holds"  (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set  "("  ($#k3_convex1 :::"conv"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "n"))))) ; 
 
theorem :: SIMPLEX2:26 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k4_topdim_1 :::"ind"::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) ;