:: PCOMPS_2  semantic presentation begin  


begin  






theorem :: PCOMPS_2:1 (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "R"))  ($#r2_wellord1 :::"well_orders"::: )  (Set (Var "A")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "A")))  ($#r2_wellord1 :::"well_orders"::: )  (Set (Var "A"))) & (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set  "(" (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "A")) ")" )))  ")" ))) ; 
 scheme  :: PCOMPS_2:sch 1 MinSet{ F1() ->    ($#m1_hidden :::"set"::: )  , F2() ->   ($#m1_hidden :::"Relation":::), P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" )) & (Bool P1[(Set (Var "X"))]) & (Bool  "("   "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" )) & (Bool P1[(Set (Var "Y"))])) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set F2 "("  ")" ))  ")" )  ")" ))
 provided
(Bool (Set F2 "("  ")" )  ($#r2_wellord1 :::"well_orders"::: )  (Set F1 "("  ")" ))
 and  
(Bool  "ex" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" )) & (Bool P1[(Set (Var "X"))])  ")" ))
 proof 


end; definitionlet "FX" be    ($#m1_hidden :::"set"::: )  ; let "R" be   ($#m1_hidden :::"Relation":::); let "B" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "FX")); func  :::"PartUnion":::  "(" "B" "," "R" ")"  ->    ($#m1_hidden :::"set"::: )   equals :: PCOMPS_2:def 1 (Set   ($#k3_tarski :::"union"::: )  (Set  "(" "R"  ($#k1_wellord1 :::"-Seg"::: )  "B" ")" )); end; 







:: deftheorem    defines :::"PartUnion"::: PCOMPS_2:def 1 :  (Bool  "for" (Set (Var "FX")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "B")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "FX")) "holds"  (Bool (Set   ($#k1_pcomps_2 :::"PartUnion"::: )   "(" (Set (Var "B")) "," (Set (Var "R")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set  "(" (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "B")) ")" )))))); 
 definitionlet "FX" be    ($#m1_hidden :::"set"::: )  ; let "R" be   ($#m1_hidden :::"Relation":::); func  :::"DisjointFam":::  "(" "FX" "," "R" ")"  ->    ($#m1_hidden :::"set"::: )   means :: PCOMPS_2:def 2 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "ex" (Set (Var "B")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" "FX" "st"  (Bool  "("  (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  "FX") & (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "B"))  ($#k6_subset_1 :::"\"::: )  (Set  "("  ($#k1_pcomps_2 :::"PartUnion"::: )   "(" (Set (Var "B")) "," "R" ")"  ")" )))  ")" ))  ")" )); end; 






:: deftheorem    defines :::"DisjointFam"::: PCOMPS_2:def 2 :  (Bool  "for" (Set (Var "FX")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "b3")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_pcomps_2 :::"DisjointFam"::: )   "(" (Set (Var "FX")) "," (Set (Var "R")) ")" )) "iff" (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) "iff" (Bool  "ex" (Set (Var "B")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "FX")) "st"  (Bool  "("  (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Var "FX"))) & (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "B"))  ($#k6_subset_1 :::"\"::: )  (Set  "("  ($#k1_pcomps_2 :::"PartUnion"::: )   "(" (Set (Var "B")) "," (Set (Var "R")) ")"  ")" )))  ")" ))  ")" ))  ")" )))); 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set (Const "X")) ")" ); func  :::"PartUnionNat":::  "(" "n" "," "f" ")"  ->    ($#m1_hidden :::"set"::: )   equals :: PCOMPS_2:def 3 (Set   ($#k3_tarski :::"union"::: )  (Set  "(" "f"  ($#k7_relat_1 :::".:"::: )  (Set  "(" (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  "n" ")" )  ($#k7_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) "n" ($#k1_tarski :::"}"::: ) ) ")" ) ")" )); end; 







:: deftheorem    defines :::"PartUnionNat"::: PCOMPS_2:def 3 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set (Var "X")) ")" ) "holds"  (Bool (Set   ($#k3_pcomps_2 :::"PartUnionNat"::: )   "(" (Set (Var "n")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relat_1 :::".:"::: )  (Set  "(" (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" )  ($#k7_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "n")) ($#k1_tarski :::"}"::: ) ) ")" ) ")" )))))); 
 begin  
















theorem :: PCOMPS_2:2 (Bool  "for" (Set (Var "PT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set (Var "PT")) "is"   ($#v9_pre_topc :::"regular"::: )  )) "holds"  (Bool  "for" (Set (Var "FX")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "PT"))  "st" (Bool (Bool (Set (Var "FX")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "PT"))) & (Bool (Set (Var "FX")) "is"   ($#v1_tops_2 :::"open"::: )  )) "holds"  (Bool  "ex" (Set (Var "HX")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "PT")) "st"  (Bool  "("  (Bool (Set (Var "HX")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "HX")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "PT"))) & (Bool  "("   "for" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "PT"))  "st" (Bool (Bool (Set (Var "V"))  ($#r2_hidden :::"in"::: )  (Set (Var "HX")))) "holds"  (Bool  "ex" (Set (Var "W")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "PT")) "st"  (Bool  "("  (Bool (Set (Var "W"))  ($#r2_hidden :::"in"::: )  (Set (Var "FX"))) & (Bool (Set   ($#k2_pre_topc :::"Cl"::: )  (Set (Var "V")))  ($#r1_tarski :::"c="::: )  (Set (Var "W")))  ")" ))  ")" )  ")" )))) ; 
 
theorem :: PCOMPS_2:3 (Bool  "for" (Set (Var "PT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "FX")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "PT"))  "st" (Bool (Bool (Set (Var "PT")) "is"   ($#v8_pre_topc :::"T_2"::: )  ) & (Bool (Set (Var "PT")) "is"   ($#v2_pcomps_1 :::"paracompact"::: )  ) & (Bool (Set (Var "FX")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "PT"))) & (Bool (Set (Var "FX")) "is"   ($#v1_tops_2 :::"open"::: )  )) "holds"  (Bool  "ex" (Set (Var "GX")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "PT")) "st"  (Bool  "("  (Bool (Set (Var "GX")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "GX")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "PT"))) & (Bool (Set   ($#k1_pcomps_1 :::"clf"::: )  (Set (Var "GX")))  ($#r1_setfam_1 :::"is_finer_than"::: )  (Set (Var "FX"))) & (Bool (Set (Var "GX")) "is"   ($#v1_pcomps_1 :::"locally_finite"::: )  )  ")" )))) ; 
 
theorem :: PCOMPS_2:4 (Bool  "for" (Set (Var "PT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "PM")) "being"   ($#l1_metric_1 :::"MetrSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "PT"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "PT"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_pcomps_1 :::"is_metric_of"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "PT")))) & (Bool (Set (Var "PM"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_pcomps_1 :::"SpaceMetr"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "PT"))) "," (Set (Var "f")) ")" ))) "holds"  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "PM")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "PT"))))))) ; 
 
theorem :: PCOMPS_2:5 (Bool  "for" (Set (Var "PT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "PM")) "being"   ($#l1_metric_1 :::"MetrSpace":::)  (Bool  "for" (Set (Var "FX")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "PT"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "PT"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "PT"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_pcomps_1 :::"is_metric_of"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "PT")))) & (Bool (Set (Var "PM"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_pcomps_1 :::"SpaceMetr"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "PT"))) "," (Set (Var "f")) ")" ))) "holds"  (Bool  "("  (Bool (Set (Var "FX")) "is"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "PT"))) "iff" (Bool (Set (Var "FX")) "is"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "PM")))  ")" ))))) ; 
 










definitionlet "PM" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "g" be   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  "(" (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set (Const "PM")) ")" ) ")" )  ($#k3_finseq_2 :::"*"::: )  ")" ); let "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); :: original: :::"."::: redefine func "g" :::"."::: "n" ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k9_setfam_1 :::"bool"::: )  (Set  "("  ($#k9_setfam_1 :::"bool"::: )  "PM" ")" )); end; scheme  :: PCOMPS_2:sch 2 XXX1{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set F1 "("  ")" ), F3(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->   ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "("  ")" ), P1[   ($#m1_hidden :::"set"::: )  ], P2[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set F1 "("  ")" ) ")" ) ")" ) "st"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k8_nat_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" )) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "f"))  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k3_tarski :::"union"::: )   "{"  (Set F3 "(" (Set (Var "c")) "," (Set (Var "n")) ")" ) where c "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) : (Bool  "for" (Set (Var "fq")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "q"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "fq"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k8_nat_1 :::"."::: )  (Set (Var "q"))))) "holds"  (Bool P2[(Set (Var "c")) "," (Set (Var "V")) "," (Set (Var "n")) "," (Set (Var "fq"))])))  "}"   ")" ) where V "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "("  ")" ) : (Bool P1[(Set (Var "V"))])  "}"  )  ")" )  ")" ))
 proof 


end; scheme  :: PCOMPS_2:sch 3 XXX{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set F1 "("  ")" ), F3(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->   ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "("  ")" ), P1[   ($#m1_hidden :::"set"::: )  ], P2[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set F1 "("  ")" ) ")" ) ")" ) "st"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k8_nat_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" )) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "f"))  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k3_tarski :::"union"::: )   "{"  (Set F3 "(" (Set (Var "c")) "," (Set (Var "n")) ")" ) where c "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) : (Bool  "("  (Bool P2[(Set (Var "c")) "," (Set (Var "V")) "," (Set (Var "n"))]) & (Bool (Bool  "not" (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )   "{"  (Set  "("  ($#k5_setfam_1 :::"union"::: )  (Set  "(" (Set (Var "f"))  ($#k8_nat_1 :::"."::: )  (Set (Var "q")) ")" ) ")" ) where q "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Set (Var "q"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))  "}"  )))  ")" )  "}"   ")" ) where V "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "("  ")" ) : (Bool P1[(Set (Var "V"))])  "}"  )  ")" )  ")" ))
 proof 


end; 
theorem :: PCOMPS_2:6 (Bool  "for" (Set (Var "PT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set (Var "PT")) "is"   ($#v3_pcomps_1 :::"metrizable"::: )  )) "holds"  (Bool  "for" (Set (Var "FX")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "PT"))  "st" (Bool (Bool (Set (Var "FX")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "PT"))) & (Bool (Set (Var "FX")) "is"   ($#v1_tops_2 :::"open"::: )  )) "holds"  (Bool  "ex" (Set (Var "GX")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "PT")) "st"  (Bool  "("  (Bool (Set (Var "GX")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "GX")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "PT"))) & (Bool (Set (Var "GX"))  ($#r1_setfam_1 :::"is_finer_than"::: )  (Set (Var "FX"))) & (Bool (Set (Var "GX")) "is"   ($#v1_pcomps_1 :::"locally_finite"::: )  )  ")" )))) ; 
 
theorem :: PCOMPS_2:7 (Bool  "for" (Set (Var "PT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set (Var "PT")) "is"   ($#v3_pcomps_1 :::"metrizable"::: )  )) "holds"  (Bool (Set (Var "PT")) "is"   ($#v2_pcomps_1 :::"paracompact"::: )  )) ;