:: COMPL_SP semantic presentation begin definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) ; let "S" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "M")); attr "S" is :::"pointwise_bounded"::: means :: COMPL_SP:def 1 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "S" ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) "is" ($#v6_tbsp_1 :::"bounded"::: ) )); end; :: deftheorem defines :::"pointwise_bounded"::: COMPL_SP:def 1 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_compl_sp :::"pointwise_bounded"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "S")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) "is" ($#v6_tbsp_1 :::"bounded"::: ) )) ")" ))); registrationlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_metric_1 :::"Reflexive"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v2_relat_1 :::"non-empty"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M")) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M"))) ($#v1_compl_sp :::"pointwise_bounded"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_metric_1 :::"Reflexive"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) ; let "S" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "M")); func :::"diameter"::: "S" -> ($#m1_subset_1 :::"Real_Sequence":::) means :: COMPL_SP:def 2 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tbsp_1 :::"diameter"::: ) (Set "(" "S" ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" )))); end; :: deftheorem defines :::"diameter"::: COMPL_SP: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 "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_compl_sp :::"diameter"::: ) (Set (Var "S")))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b3")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tbsp_1 :::"diameter"::: ) (Set "(" (Set (Var "S")) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" )))) ")" )))); theorem :: COMPL_SP:1 (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_compl_sp :::"pointwise_bounded"::: ) ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "M")) "holds" (Bool (Set ($#k1_compl_sp :::"diameter"::: ) (Set (Var "S"))) "is" ($#v2_seq_2 :::"bounded_below"::: ) ))) ; theorem :: COMPL_SP: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 "S")) "being" ($#v1_compl_sp :::"pointwise_bounded"::: ) ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "S")) "is" bbbadV2_PROB_1())) "holds" (Bool "(" (Bool (Set ($#k1_compl_sp :::"diameter"::: ) (Set (Var "S"))) "is" ($#v1_seq_2 :::"bounded_above"::: ) ) & (Bool (Set ($#k1_compl_sp :::"diameter"::: ) (Set (Var "S"))) "is" bbbadV8_VALUED_0()) ")" ))) ; theorem :: COMPL_SP: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 "S")) "being" ($#v1_compl_sp :::"pointwise_bounded"::: ) ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "S")) "is" bbbadV3_PROB_1())) "holds" (Bool (Set ($#k1_compl_sp :::"diameter"::: ) (Set (Var "S"))) "is" bbbadV7_VALUED_0()))) ; theorem :: COMPL_SP: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_compl_sp :::"pointwise_bounded"::: ) ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "S")) "is" bbbadV2_PROB_1()) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k1_compl_sp :::"diameter"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "M")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "S")) ($#k8_nat_1 :::"."::: ) (Set (Var "i")))) ")" )) "holds" (Bool (Set (Var "F")) "is" ($#v3_tbsp_1 :::"Cauchy"::: ) )))) ; theorem :: COMPL_SP:5 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_metric_1 :::"Reflexive"::: ) ($#v8_metric_1 :::"symmetric"::: ) ($#v9_metric_1 :::"triangle"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r")))) "holds" (Bool (Set ($#k3_tbsp_1 :::"diameter"::: ) (Set "(" ($#k10_metric_1 :::"cl_Ball"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "r"))))))) ; definitionlet "M" be ($#l1_metric_1 :::"MetrStruct"::: ) ; let "U" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "M")); attr "U" is :::"open"::: means :: COMPL_SP:def 3 (Bool "U" ($#r2_hidden :::"in"::: ) (Set ($#k2_pcomps_1 :::"Family_open_set"::: ) "M")); end; :: deftheorem defines :::"open"::: COMPL_SP:def 3 : (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "U")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "U")) "is" ($#v2_compl_sp :::"open"::: ) ) "iff" (Bool (Set (Var "U")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pcomps_1 :::"Family_open_set"::: ) (Set (Var "M")))) ")" ))); definitionlet "M" be ($#l1_metric_1 :::"MetrStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "M")); attr "A" is :::"closed"::: means :: COMPL_SP:def 4 (Bool (Set "A" ($#k3_subset_1 :::"`"::: ) ) "is" ($#v2_compl_sp :::"open"::: ) ); end; :: deftheorem defines :::"closed"::: COMPL_SP:def 4 : (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_compl_sp :::"closed"::: ) ) "iff" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v2_compl_sp :::"open"::: ) ) ")" ))); registrationlet "M" be ($#l1_metric_1 :::"MetrStruct"::: ) ; cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v2_compl_sp :::"open"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M")); cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v3_compl_sp :::"closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M")); end; registrationlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compl_sp :::"open"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_compl_sp :::"closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M")); end; theorem :: COMPL_SP:6 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "A9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "A9")) ($#r1_hidden :::"="::: ) (Set (Var "A")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "A")) "is" ($#v2_compl_sp :::"open"::: ) )) "implies" (Bool (Set (Var "A9")) "is" ($#v3_pre_topc :::"open"::: ) ) ")" & "(" (Bool (Bool (Set (Var "A9")) "is" ($#v3_pre_topc :::"open"::: ) )) "implies" (Bool (Set (Var "A")) "is" ($#v2_compl_sp :::"open"::: ) ) ")" & "(" (Bool (Bool (Set (Var "A")) "is" ($#v3_compl_sp :::"closed"::: ) )) "implies" (Bool (Set (Var "A9")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" & "(" (Bool (Bool (Set (Var "A9")) "is" ($#v4_pre_topc :::"closed"::: ) )) "implies" (Bool (Set (Var "A")) "is" ($#v3_compl_sp :::"closed"::: ) ) ")" ")" )))) ; definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "S" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "T")); attr "S" is :::"open"::: means :: COMPL_SP:def 5 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "S" ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) "is" ($#v3_pre_topc :::"open"::: ) )); attr "S" is :::"closed"::: means :: COMPL_SP:def 6 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "S" ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) "is" ($#v4_pre_topc :::"closed"::: ) )); end; :: deftheorem defines :::"open"::: COMPL_SP:def 5 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v4_compl_sp :::"open"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "S")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) "is" ($#v3_pre_topc :::"open"::: ) )) ")" ))); :: deftheorem defines :::"closed"::: COMPL_SP:def 6 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v5_compl_sp :::"closed"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "S")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) "is" ($#v4_pre_topc :::"closed"::: ) )) ")" ))); registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T"))) ($#v4_compl_sp :::"open"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T"))) ($#v5_compl_sp :::"closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v2_relat_1 :::"non-empty"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T"))) ($#v4_compl_sp :::"open"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v2_relat_1 :::"non-empty"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T"))) ($#v5_compl_sp :::"closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "M" be ($#l1_metric_1 :::"MetrStruct"::: ) ; let "S" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "M")); attr "S" is :::"open"::: means :: COMPL_SP:def 7 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "S" ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) "is" ($#v2_compl_sp :::"open"::: ) )); attr "S" is :::"closed"::: means :: COMPL_SP:def 8 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "S" ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) "is" ($#v3_compl_sp :::"closed"::: ) )); end; :: deftheorem defines :::"open"::: COMPL_SP:def 7 : (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v6_compl_sp :::"open"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "S")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) "is" ($#v2_compl_sp :::"open"::: ) )) ")" ))); :: deftheorem defines :::"closed"::: COMPL_SP:def 8 : (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v7_compl_sp :::"closed"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "S")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) "is" ($#v3_compl_sp :::"closed"::: ) )) ")" ))); registrationlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v2_relat_1 :::"non-empty"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M")) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M"))) ($#v1_compl_sp :::"pointwise_bounded"::: ) ($#v6_compl_sp :::"open"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v2_relat_1 :::"non-empty"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M")) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M"))) ($#v1_compl_sp :::"pointwise_bounded"::: ) ($#v7_compl_sp :::"closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: COMPL_SP:7 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "S9")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "S9")) ($#r1_funct_2 :::"="::: ) (Set (Var "S")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "S")) "is" ($#v6_compl_sp :::"open"::: ) )) "implies" (Bool (Set (Var "S9")) "is" ($#v4_compl_sp :::"open"::: ) ) ")" & "(" (Bool (Bool (Set (Var "S9")) "is" ($#v4_compl_sp :::"open"::: ) )) "implies" (Bool (Set (Var "S")) "is" ($#v6_compl_sp :::"open"::: ) ) ")" & "(" (Bool (Bool (Set (Var "S")) "is" ($#v7_compl_sp :::"closed"::: ) )) "implies" (Bool (Set (Var "S9")) "is" ($#v5_compl_sp :::"closed"::: ) ) ")" & "(" (Bool (Bool (Set (Var "S9")) "is" ($#v5_compl_sp :::"closed"::: ) )) "implies" (Bool (Set (Var "S")) "is" ($#v7_compl_sp :::"closed"::: ) ) ")" ")" )))) ; theorem :: COMPL_SP:8 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_metric_1 :::"Reflexive"::: ) ($#v8_metric_1 :::"symmetric"::: ) ($#v9_metric_1 :::"triangle"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "CL")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v6_tbsp_1 :::"bounded"::: ) )) "holds" (Bool "for" (Set (Var "S9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Var "S9"))) & (Bool (Set (Var "CL")) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "S9"))))) "holds" (Bool "(" (Bool (Set (Var "CL")) "is" ($#v6_tbsp_1 :::"bounded"::: ) ) & (Bool (Set ($#k3_tbsp_1 :::"diameter"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tbsp_1 :::"diameter"::: ) (Set (Var "CL")))) ")" )))) ; begin theorem :: COMPL_SP:9 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "M")) (Bool "ex" (Set (Var "S")) "being" ($#v2_relat_1 :::"non-empty"::: ) ($#v7_compl_sp :::"closed"::: ) ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "S")) "is" bbbadV2_PROB_1()) & "(" (Bool (Bool (Set (Var "C")) "is" ($#v3_tbsp_1 :::"Cauchy"::: ) )) "implies" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_compl_sp :::"pointwise_bounded"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k1_compl_sp :::"diameter"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "ex" (Set (Var "U")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool "(" (Bool (Set (Var "U")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "C")) ($#k3_funct_2 :::"."::: ) (Set (Var "j")) ")" ) where j "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "j")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "i"))) "}" ) & (Bool (Set (Set (Var "S")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "U")))) ")" )) ")" ) ")" )))) ; theorem :: COMPL_SP:10 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v4_tbsp_1 :::"complete"::: ) ) "iff" (Bool "for" (Set (Var "S")) "being" ($#v2_relat_1 :::"non-empty"::: ) ($#v1_compl_sp :::"pointwise_bounded"::: ) ($#v7_compl_sp :::"closed"::: ) ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "S")) "is" bbbadV2_PROB_1()) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k1_compl_sp :::"diameter"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "not" (Bool (Set ($#k2_kurato_0 :::"meet"::: ) (Set (Var "S"))) "is" ($#v1_xboole_0 :::"empty"::: ) ))) ")" )) ; theorem :: COMPL_SP:11 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "S")) "being" ($#v2_relat_1 :::"non-empty"::: ) ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "S")) "is" bbbadV2_PROB_1())) "holds" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Var "F")) "is" ($#v3_finset_1 :::"centered"::: ) )))) ; theorem :: COMPL_SP:12 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "M")) (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")) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "S"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "S")) "is" ($#v6_compl_sp :::"open"::: ) )) "implies" (Bool (Set (Var "F")) "is" ($#v1_tops_2 :::"open"::: ) ) ")" & "(" (Bool (Bool (Set (Var "S")) "is" ($#v7_compl_sp :::"closed"::: ) )) "implies" (Bool (Set (Var "F")) "is" ($#v2_tops_2 :::"closed"::: ) ) ")" ")" )))) ; theorem :: COMPL_SP:13 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "R")) "is" bbbadV2_PROB_1()) & "(" (Bool (Bool (Set (Var "F")) "is" ($#v3_finset_1 :::"centered"::: ) )) "implies" (Bool (Set (Var "R")) "is" ($#v2_relat_1 :::"non-empty"::: ) ) ")" & "(" (Bool (Bool (Set (Var "F")) "is" ($#v1_tops_2 :::"open"::: ) )) "implies" (Bool (Set (Var "R")) "is" ($#v4_compl_sp :::"open"::: ) ) ")" & "(" (Bool (Bool (Set (Var "F")) "is" ($#v2_tops_2 :::"closed"::: ) )) "implies" (Bool (Set (Var "R")) "is" ($#v5_compl_sp :::"closed"::: ) ) ")" & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "R")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" (Set (Var "S")) ($#k3_funct_2 :::"."::: ) (Set (Var "j")) ")" ) where j "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) "}" )) ")" ) ")" ))))) ; theorem :: COMPL_SP:14 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v4_tbsp_1 :::"complete"::: ) ) "iff" (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" ($#v2_tops_2 :::"closed"::: ) ) & (Bool (Set (Var "F")) "is" ($#v3_finset_1 :::"centered"::: ) ) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "A")) "is" ($#v6_tbsp_1 :::"bounded"::: ) ) & (Bool (Set ($#k3_tbsp_1 :::"diameter"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" )) ")" )) "holds" (Bool "not" (Bool (Set ($#k6_setfam_1 :::"meet"::: ) (Set (Var "F"))) "is" ($#v1_xboole_0 :::"empty"::: ) ))) ")" )) ; theorem :: COMPL_SP:15 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "B9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "M")) ($#k1_topmetr :::"|"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "B9")))) "holds" (Bool "(" (Bool (Set (Var "B9")) "is" ($#v6_tbsp_1 :::"bounded"::: ) ) "iff" (Bool (Set (Var "B")) "is" ($#v6_tbsp_1 :::"bounded"::: ) ) ")" ))))) ; theorem :: COMPL_SP:16 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "B9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "M")) ($#k1_topmetr :::"|"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "B9"))) & (Bool (Set (Var "B")) "is" ($#v6_tbsp_1 :::"bounded"::: ) )) "holds" (Bool (Set ($#k3_tbsp_1 :::"diameter"::: ) (Set (Var "B9"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_tbsp_1 :::"diameter"::: ) (Set (Var "B")))))))) ; theorem :: COMPL_SP:17 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" (Set (Var "M")) ($#k1_topmetr :::"|"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set (Var "S")) "is" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "M")))))) ; theorem :: COMPL_SP:18 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" (Set (Var "M")) ($#k1_topmetr :::"|"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "S9")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "S")) ($#r1_funct_2 :::"="::: ) (Set (Var "S9")))) "holds" (Bool "(" (Bool (Set (Var "S9")) "is" ($#v3_tbsp_1 :::"Cauchy"::: ) ) "iff" (Bool (Set (Var "S")) "is" ($#v3_tbsp_1 :::"Cauchy"::: ) ) ")" ))))) ; theorem :: COMPL_SP:19 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) "st" (Bool (Bool (Set (Var "M")) "is" ($#v4_tbsp_1 :::"complete"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "A9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "A9")))) "holds" (Bool "(" (Bool (Set (Set (Var "M")) ($#k1_topmetr :::"|"::: ) (Set (Var "A"))) "is" ($#v4_tbsp_1 :::"complete"::: ) ) "iff" (Bool (Set (Var "A9")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" )))) ; begin definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; attr "T" is :::"countably_compact"::: means :: COMPL_SP:def 9 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" "T" "st" (Bool (Bool (Set (Var "F")) "is" ($#m1_setfam_1 :::"Cover":::) "of" "T") & (Bool (Set (Var "F")) "is" ($#v1_tops_2 :::"open"::: ) ) & (Bool (Set (Var "F")) "is" ($#v4_card_3 :::"countable"::: ) )) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" "T" "st" (Bool "(" (Bool (Set (Var "G")) ($#r1_tarski :::"c="::: ) (Set (Var "F"))) & (Bool (Set (Var "G")) "is" ($#m1_setfam_1 :::"Cover":::) "of" "T") & (Bool (Set (Var "G")) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ))); end; :: deftheorem defines :::"countably_compact"::: COMPL_SP:def 9 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v8_compl_sp :::"countably_compact"::: ) ) "iff" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "T"))) & (Bool (Set (Var "F")) "is" ($#v1_tops_2 :::"open"::: ) ) & (Bool (Set (Var "F")) "is" ($#v4_card_3 :::"countable"::: ) )) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "G")) ($#r1_tarski :::"c="::: ) (Set (Var "F"))) & (Bool (Set (Var "G")) "is" ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "T"))) & (Bool (Set (Var "G")) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ))) ")" )); theorem :: COMPL_SP:20 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v1_compts_1 :::"compact"::: ) )) "holds" (Bool (Set (Var "T")) "is" ($#v8_compl_sp :::"countably_compact"::: ) )) ; theorem :: COMPL_SP:21 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v8_compl_sp :::"countably_compact"::: ) ) "iff" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v3_finset_1 :::"centered"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_tops_2 :::"closed"::: ) ) & (Bool (Set (Var "F")) "is" ($#v4_card_3 :::"countable"::: ) )) "holds" (Bool (Set ($#k6_setfam_1 :::"meet"::: ) (Set (Var "F"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" )) ; theorem :: COMPL_SP:22 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v8_compl_sp :::"countably_compact"::: ) ) "iff" (Bool "for" (Set (Var "S")) "being" ($#v2_relat_1 :::"non-empty"::: ) ($#v5_compl_sp :::"closed"::: ) ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "S")) "is" bbbadV2_PROB_1())) "holds" (Bool (Set ($#k2_kurato_0 :::"meet"::: ) (Set (Var "S"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" )) ; theorem :: COMPL_SP:23 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set (Var "F"))) & (Bool (Set (Var "S")) "is" ($#v2_relat_1 :::"non-empty"::: ) )) "holds" (Bool "ex" (Set (Var "R")) "being" ($#v2_relat_1 :::"non-empty"::: ) ($#v5_compl_sp :::"closed"::: ) ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "R")) "is" bbbadV2_PROB_1()) & "(" (Bool (Bool (Set (Var "F")) "is" ($#v1_pcomps_1 :::"locally_finite"::: ) ) & (Bool (Set (Var "S")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "implies" (Bool (Set ($#k2_kurato_0 :::"meet"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "ex" (Set (Var "Si")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Set (Var "R")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set (Var "Si")) ")" ))) & (Bool (Set (Var "Si")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "S")) ($#k3_funct_2 :::"."::: ) (Set (Var "j")) ")" ) where j "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "j")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "i"))) "}" ) ")" )) ")" ) ")" ))))) ; theorem :: COMPL_SP:24 canceled; theorem :: COMPL_SP:25 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) "is" bbbadV2_PROB_1())) "holds" (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "S")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) ")" ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "S"))) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool "not" (Bool (Set ($#k2_kurato_0 :::"meet"::: ) (Set (Var "F"))) "is" ($#v1_xboole_0 :::"empty"::: ) ))))) ; theorem :: COMPL_SP:26 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v8_compl_sp :::"countably_compact"::: ) ) "iff" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_pcomps_1 :::"locally_finite"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setfam_1 :::"with_non-empty_elements"::: ) )) "holds" (Bool (Set (Var "F")) "is" ($#v1_finset_1 :::"finite"::: ) )) ")" )) ; theorem :: COMPL_SP:27 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v8_compl_sp :::"countably_compact"::: ) ) "iff" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_pcomps_1 :::"locally_finite"::: ) ) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" )) "holds" (Bool (Set (Var "F")) "is" ($#v1_finset_1 :::"finite"::: ) )) ")" )) ; theorem :: COMPL_SP:28 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_pre_topc :::"T_1"::: ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v8_compl_sp :::"countably_compact"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_finset_1 :::"infinite"::: ) )) "holds" (Bool "not" (Bool (Set ($#k2_topgen_1 :::"Der"::: ) (Set (Var "A"))) "is" ($#v1_xboole_0 :::"empty"::: ) ))) ")" )) ; theorem :: COMPL_SP:29 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_pre_topc :::"T_1"::: ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v8_compl_sp :::"countably_compact"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_finset_1 :::"infinite"::: ) ) & (Bool (Set (Var "A")) "is" ($#v4_card_3 :::"countable"::: ) )) "holds" (Bool "not" (Bool (Set ($#k2_topgen_1 :::"Der"::: ) (Set (Var "A"))) "is" ($#v1_xboole_0 :::"empty"::: ) ))) ")" )) ; scheme :: COMPL_SP:sch 1 Th39{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) ")" )) ")" ) ")" )) provided (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) "iff" (Bool P1[(Set (Var "y")) "," (Set (Var "x"))]) ")" )) and (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool P1[(Set (Var "x")) "," (Set (Var "x"))])) proof end; theorem :: COMPL_SP:30 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_metric_1 :::"Reflexive"::: ) ($#v8_metric_1 :::"symmetric"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "st" (Bool "(" (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r"))) ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "q")) "," (Set (Var "r")) ")" )) ")" )) ")" ) ")" )))) ; theorem :: COMPL_SP:31 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_metric_1 :::"Reflexive"::: ) ($#v8_metric_1 :::"symmetric"::: ) ($#v9_metric_1 :::"triangle"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v1_tbsp_1 :::"totally_bounded"::: ) ) "iff" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r"))) ")" )) "holds" (Bool (Set (Var "A")) "is" ($#v1_finset_1 :::"finite"::: ) ))) ")" )) ; theorem :: COMPL_SP:32 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_metric_1 :::"Reflexive"::: ) ($#v8_metric_1 :::"symmetric"::: ) ($#v9_metric_1 :::"triangle"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) "st" (Bool (Bool (Set ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M"))) "is" ($#v8_compl_sp :::"countably_compact"::: ) )) "holds" (Bool (Set (Var "M")) "is" ($#v1_tbsp_1 :::"totally_bounded"::: ) )) ; theorem :: COMPL_SP:33 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) "st" (Bool (Bool (Set (Var "M")) "is" ($#v1_tbsp_1 :::"totally_bounded"::: ) )) "holds" (Bool (Set ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M"))) "is" ($#v5_waybel23 :::"second-countable"::: ) )) ; theorem :: COMPL_SP:34 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "T")) "is" ($#v5_waybel23 :::"second-countable"::: ) )) "holds" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "F")) "is" ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "T"))) & (Bool (Set (Var "F")) "is" ($#v1_tops_2 :::"open"::: ) )) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "G")) ($#r1_tarski :::"c="::: ) (Set (Var "F"))) & (Bool (Set (Var "G")) "is" ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "T"))) & (Bool (Set (Var "G")) "is" ($#v4_card_3 :::"countable"::: ) ) ")" )))) ; begin theorem :: COMPL_SP:35 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) "holds" (Bool "(" (Bool (Set ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M"))) "is" ($#v1_compts_1 :::"compact"::: ) ) "iff" (Bool (Set ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M"))) "is" ($#v8_compl_sp :::"countably_compact"::: ) ) ")" )) ; theorem :: COMPL_SP:36 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_finset_1 :::"infinite"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "F"))))) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Set (Var "Y")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A"))) "is" ($#v1_finset_1 :::"infinite"::: ) ) ")" ))))) ; theorem :: COMPL_SP:37 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) "holds" (Bool "(" (Bool (Set ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set (Var "M"))) "is" ($#v1_compts_1 :::"compact"::: ) ) "iff" (Bool "(" (Bool (Set (Var "M")) "is" ($#v1_tbsp_1 :::"totally_bounded"::: ) ) & (Bool (Set (Var "M")) "is" ($#v4_tbsp_1 :::"complete"::: ) ) ")" ) ")" )) ; begin theorem :: COMPL_SP:38 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "X")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )) & (Bool "(" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) ")" ) "or" (Bool "(" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ) ")" ) ")" ))) ")" ))))) ; definitionlet "M" be ($#l1_metric_1 :::"MetrStruct"::: ) ; let "a" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "M")); let "X" be ($#m1_hidden :::"set"::: ) ; func :::"well_dist"::: "(" "a" "," "X" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) "a" ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) "X" "," "a" ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) "a" ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) "X" "," "a" ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: COMPL_SP:def 10 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) "a" ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) "X" "," "a" ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )) (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Point":::) "of" "M" "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "y1")))) "implies" (Bool (Set it ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_metric_1 :::"dist"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" )) ")" & "(" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "y1")))) "implies" (Bool (Set it ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_metric_1 :::"dist"::: ) "(" (Set (Var "x2")) "," "a" ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k2_metric_1 :::"dist"::: ) "(" "a" "," (Set (Var "y2")) ")" ")" ))) ")" ")" )))); end; :: deftheorem defines :::"well_dist"::: COMPL_SP:def 10 : (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "X")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "X")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_compl_sp :::"well_dist"::: ) "(" (Set (Var "a")) "," (Set (Var "X")) ")" )) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "X")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )) (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "y1")))) "implies" (Bool (Set (Set (Var "b4")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_metric_1 :::"dist"::: ) "(" (Set (Var "x2")) "," (Set (Var "y2")) ")" )) ")" & "(" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "y1")))) "implies" (Bool (Set (Set (Var "b4")) ($#k1_metric_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_metric_1 :::"dist"::: ) "(" (Set (Var "x2")) "," (Set (Var "a")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k2_metric_1 :::"dist"::: ) "(" (Set (Var "a")) "," (Set (Var "y2")) ")" ")" ))) ")" ")" )))) ")" ))))); theorem :: COMPL_SP:39 (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k2_compl_sp :::"well_dist"::: ) "(" (Set (Var "a")) "," (Set (Var "X")) ")" ) "is" ($#v2_metric_1 :::"Reflexive"::: ) )) "implies" (Bool (Set (Var "M")) "is" ($#v6_metric_1 :::"Reflexive"::: ) ) ")" & "(" (Bool (Bool (Set ($#k2_compl_sp :::"well_dist"::: ) "(" (Set (Var "a")) "," (Set (Var "X")) ")" ) "is" ($#v4_metric_1 :::"symmetric"::: ) )) "implies" (Bool (Set (Var "M")) "is" ($#v8_metric_1 :::"symmetric"::: ) ) ")" & "(" (Bool (Bool (Set ($#k2_compl_sp :::"well_dist"::: ) "(" (Set (Var "a")) "," (Set (Var "X")) ")" ) "is" ($#v5_metric_1 :::"triangle"::: ) ) & (Bool (Set ($#k2_compl_sp :::"well_dist"::: ) "(" (Set (Var "a")) "," (Set (Var "X")) ")" ) "is" ($#v2_metric_1 :::"Reflexive"::: ) )) "implies" (Bool (Set (Var "M")) "is" ($#v9_metric_1 :::"triangle"::: ) ) ")" & "(" (Bool (Bool (Set ($#k2_compl_sp :::"well_dist"::: ) "(" (Set (Var "a")) "," (Set (Var "X")) ")" ) "is" ($#v3_metric_1 :::"discerning"::: ) ) & (Bool (Set ($#k2_compl_sp :::"well_dist"::: ) "(" (Set (Var "a")) "," (Set (Var "X")) ")" ) "is" ($#v2_metric_1 :::"Reflexive"::: ) )) "implies" (Bool (Set (Var "M")) "is" ($#v7_metric_1 :::"discerning"::: ) ) ")" ")" )))) ; definitionlet "M" be ($#l1_metric_1 :::"MetrStruct"::: ) ; let "a" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "M")); let "X" be ($#m1_hidden :::"set"::: ) ; func :::"WellSpace"::: "(" "a" "," "X" ")" -> ($#v1_metric_1 :::"strict"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) equals :: COMPL_SP:def 11 (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) "a" ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) "X" "," "a" ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set "(" ($#k2_compl_sp :::"well_dist"::: ) "(" "a" "," "X" ")" ")" ) "#)" ); end; :: deftheorem defines :::"WellSpace"::: COMPL_SP:def 11 : (Bool "for" (Set (Var "M")) "being" ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_compl_sp :::"WellSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_metric_1 :::"MetrStruct"::: ) "(#" (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "X")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set "(" ($#k2_compl_sp :::"well_dist"::: ) "(" (Set (Var "a")) "," (Set (Var "X")) ")" ")" ) "#)" ))))); registrationlet "M" be ($#l1_metric_1 :::"MetrStruct"::: ) ; let "a" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "M")); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_compl_sp :::"WellSpace"::: ) "(" "a" "," "X" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_metric_1 :::"strict"::: ) ; end; registrationlet "M" be ($#v6_metric_1 :::"Reflexive"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) ; let "a" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "M")); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_compl_sp :::"WellSpace"::: ) "(" "a" "," "X" ")" ) -> ($#v1_metric_1 :::"strict"::: ) ($#v6_metric_1 :::"Reflexive"::: ) ; end; registrationlet "M" be ($#v8_metric_1 :::"symmetric"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) ; let "a" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "M")); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_compl_sp :::"WellSpace"::: ) "(" "a" "," "X" ")" ) -> ($#v1_metric_1 :::"strict"::: ) ($#v8_metric_1 :::"symmetric"::: ) ; end; registrationlet "M" be ($#v6_metric_1 :::"Reflexive"::: ) ($#v8_metric_1 :::"symmetric"::: ) ($#v9_metric_1 :::"triangle"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) ; let "a" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "M")); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_compl_sp :::"WellSpace"::: ) "(" "a" "," "X" ")" ) -> ($#v1_metric_1 :::"strict"::: ) ($#v9_metric_1 :::"triangle"::: ) ; end; registrationlet "M" be ($#l1_metric_1 :::"MetrSpace":::); let "a" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "M")); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_compl_sp :::"WellSpace"::: ) "(" "a" "," "X" ")" ) -> ($#v1_metric_1 :::"strict"::: ) ($#v7_metric_1 :::"discerning"::: ) ; end; theorem :: COMPL_SP:40 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_metric_1 :::"Reflexive"::: ) ($#v9_metric_1 :::"triangle"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k3_compl_sp :::"WellSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "X")) ")" ) "is" ($#v4_tbsp_1 :::"complete"::: ) )) "holds" (Bool (Set (Var "M")) "is" ($#v4_tbsp_1 :::"complete"::: ) )))) ; theorem :: COMPL_SP:41 (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"::: ) ($#v8_metric_1 :::"symmetric"::: ) ($#v9_metric_1 :::"triangle"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k3_compl_sp :::"WellSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "X")) ")" ")" ) "holds" (Bool "(" "not" (Bool (Set (Var "S")) "is" ($#v3_tbsp_1 :::"Cauchy"::: ) ) "or" (Bool "for" (Set (Var "Xa")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k3_compl_sp :::"WellSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "X")) ")" ")" ) "st" (Bool (Bool (Set (Var "Xa")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "X")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "n")))) "holds" (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set "(" (Set (Var "S")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ) "," (Set (Var "Xa")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))))))) "or" (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::)(Bool "ex" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "n")))) "holds" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Set (Set (Var "S")) ($#k8_nat_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "Y")) "," (Set (Var "p")) ($#k4_tarski :::"]"::: ) )))))) ")" ))))) ; theorem :: COMPL_SP:42 (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"::: ) ($#v8_metric_1 :::"symmetric"::: ) ($#v9_metric_1 :::"triangle"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "M")) "is" ($#v4_tbsp_1 :::"complete"::: ) )) "holds" (Bool (Set ($#k3_compl_sp :::"WellSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "X")) ")" ) "is" ($#v4_tbsp_1 :::"complete"::: ) )))) ; theorem :: COMPL_SP:43 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_metric_1 :::"Reflexive"::: ) ($#v8_metric_1 :::"symmetric"::: ) ($#v9_metric_1 :::"triangle"::: ) ($#l1_metric_1 :::"MetrStruct"::: ) "st" (Bool (Bool (Set (Var "M")) "is" ($#v4_tbsp_1 :::"complete"::: ) )) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "holds" (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"infinite"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k3_compl_sp :::"WellSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "X")) ")" ) "is" ($#v4_tbsp_1 :::"complete"::: ) ) & (Bool "ex" (Set (Var "S")) "being" ($#v2_relat_1 :::"non-empty"::: ) ($#v1_compl_sp :::"pointwise_bounded"::: ) ($#m1_subset_1 :::"SetSequence":::) "of" (Set "(" ($#k3_compl_sp :::"WellSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "X")) ")" ")" ) "st" (Bool "(" (Bool (Set (Var "S")) "is" ($#v7_compl_sp :::"closed"::: ) ) & (Bool (Set (Var "S")) "is" bbbadV2_PROB_1()) & (Bool (Set ($#k2_kurato_0 :::"meet"::: ) (Set (Var "S"))) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) ")" )))) ; theorem :: COMPL_SP:44 (Bool "ex" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_metric_1 :::"MetrSpace":::) "st" (Bool "(" (Bool (Set (Var "M")) "is" ($#v4_tbsp_1 :::"complete"::: ) ) & (Bool "ex" (Set (Var "S")) "being" ($#v2_relat_1 :::"non-empty"::: ) ($#v1_compl_sp :::"pointwise_bounded"::: ) ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "S")) "is" ($#v7_compl_sp :::"closed"::: ) ) & (Bool (Set (Var "S")) "is" bbbadV2_PROB_1()) & (Bool (Set ($#k2_kurato_0 :::"meet"::: ) (Set (Var "S"))) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" )) ")" )) ;