:: YELLOW17  semantic presentation begin  
theorem :: YELLOW17:1 (Bool  "for" (Set (Var "F")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "i")) "," (Set (Var "xi")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Ai")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" )  "st" (Bool (Bool (Set (Set  "("  ($#k12_card_3 :::"proj"::: )   "(" (Set (Var "F")) "," (Set (Var "i")) ")"  ")" )  ($#k8_relat_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "xi")) ($#k1_tarski :::"}"::: ) ))  ($#r1_xboole_0 :::"meets"::: )  (Set (Set  "("  ($#k12_card_3 :::"proj"::: )   "(" (Set (Var "F")) "," (Set (Var "i")) ")"  ")" )  ($#k8_relat_1 :::"""::: )  (Set (Var "Ai"))))) "holds"  (Bool (Set (Var "xi"))  ($#r2_hidden :::"in"::: )  (Set (Var "Ai")))))) ; 
 
theorem :: YELLOW17:2 (Bool  "for" (Set (Var "F")) "," (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "i")) "," (Set (Var "xi")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "xi"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))) & (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_card_3 :::"product"::: )  (Set (Var "F"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_funct_7 :::"+*"::: )   "(" (Set (Var "i")) "," (Set (Var "xi")) ")" )  ($#r2_hidden :::"in"::: )  (Set   ($#k4_card_3 :::"product"::: )  (Set (Var "F")))))) ; 
 
theorem :: YELLOW17:3 (Bool  "for" (Set (Var "F")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "i")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "F"))))) "holds"  (Bool  "("  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k12_card_3 :::"proj"::: )   "(" (Set (Var "F")) "," (Set (Var "i")) ")"  ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))) &  "("  (Bool (Bool (Set   ($#k4_card_3 :::"product"::: )  (Set (Var "F")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "implies" (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k12_card_3 :::"proj"::: )   "(" (Set (Var "F")) "," (Set (Var "i")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i"))))  ")"   ")" ))) ; 
 
theorem :: YELLOW17:4 (Bool  "for" (Set (Var "F")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "i")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "F"))))) "holds"  (Bool (Set (Set  "("  ($#k12_card_3 :::"proj"::: )   "(" (Set (Var "F")) "," (Set (Var "i")) ")"  ")" )  ($#k8_relat_1 :::"""::: )  (Set  "(" (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_card_3 :::"product"::: )  (Set (Var "F")))))) ; 
 
theorem :: YELLOW17:5 (Bool  "for" (Set (Var "F")) "," (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "i")) "," (Set (Var "xi")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "xi"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))) & (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "F")))) & (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_card_3 :::"product"::: )  (Set (Var "F"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_funct_7 :::"+*"::: )   "(" (Set (Var "i")) "," (Set (Var "xi")) ")" )  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k12_card_3 :::"proj"::: )   "(" (Set (Var "F")) "," (Set (Var "i")) ")"  ")" )  ($#k8_relat_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "xi")) ($#k1_tarski :::"}"::: ) ))))) ; 
 
theorem :: YELLOW17:6 (Bool  "for" (Set (Var "F")) "," (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "xi1")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Ai2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i2")) ")" )  "st" (Bool (Bool (Set (Var "xi1"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i1")))) & (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_card_3 :::"product"::: )  (Set (Var "F")))) & (Bool (Set (Var "i1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "i2")))) "holds"  (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k12_card_3 :::"proj"::: )   "(" (Set (Var "F")) "," (Set (Var "i2")) ")"  ")" )  ($#k8_relat_1 :::"""::: )  (Set (Var "Ai2")))) "iff" (Bool (Set (Set (Var "f"))  ($#k2_funct_7 :::"+*"::: )   "(" (Set (Var "i1")) "," (Set (Var "xi1")) ")" )  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k12_card_3 :::"proj"::: )   "(" (Set (Var "F")) "," (Set (Var "i2")) ")"  ")" )  ($#k8_relat_1 :::"""::: )  (Set (Var "Ai2"))))  ")" )))) ; 
 
theorem :: YELLOW17:7 (Bool  "for" (Set (Var "F")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "xi1")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Ai2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i2")) ")" )  "st" (Bool (Bool (Set   ($#k4_card_3 :::"product"::: )  (Set (Var "F")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "xi1"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i1")))) & (Bool (Set (Var "i1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "F")))) & (Bool (Set (Var "i2"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "F")))) & (Bool (Set (Var "Ai2"))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i2"))))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k12_card_3 :::"proj"::: )   "(" (Set (Var "F")) "," (Set (Var "i1")) ")"  ")" )  ($#k8_relat_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "xi1")) ($#k1_tarski :::"}"::: ) ))  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k12_card_3 :::"proj"::: )   "(" (Set (Var "F")) "," (Set (Var "i2")) ")"  ")" )  ($#k8_relat_1 :::"""::: )  (Set (Var "Ai2")))) "iff" (Bool  "("  (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set (Var "i2"))) & (Bool (Set (Var "xi1"))  ($#r2_hidden :::"in"::: )  (Set (Var "Ai2")))  ")" )  ")" )))) ; 
 scheme  :: YELLOW17:sch 1 ElProductEx{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_waybel18 :::"TopStruct-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set F1 "("  ")" ), P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k3_waybel18 :::"product"::: )  (Set F2 "("  ")" ) ")" ) "st"  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) "holds"  (Bool P1[(Set (Set (Var "f"))  ($#k5_waybel18 :::"."::: )  (Set (Var "i"))) "," (Set (Var "i"))])))
 provided
(Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set F2 "("  ")" )  ($#k4_waybel18 :::"."::: )  (Set (Var "i")) ")" ) "st" (Bool P1[(Set (Var "x")) "," (Set (Var "i"))])))
 proof 


end; 
theorem :: YELLOW17:8 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_waybel18 :::"TopStruct-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k3_waybel18 :::"product"::: )  (Set (Var "J")) ")" ) "holds"  (Bool (Set (Set  "("  ($#k6_waybel18 :::"proj"::: )   "(" (Set (Var "J")) "," (Set (Var "i")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k5_waybel18 :::"."::: )  (Set (Var "i")))))))) ; 
 
theorem :: YELLOW17:9 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_waybel18 :::"TopStruct-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I"))  (Bool  "for" (Set (Var "xi")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "J"))  ($#k4_waybel18 :::"."::: )  (Set (Var "i")) ")" )  (Bool  "for" (Set (Var "Ai")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "J"))  ($#k4_waybel18 :::"."::: )  (Set (Var "i")) ")" )  "st" (Bool (Bool (Set (Set  "("  ($#k6_waybel18 :::"proj"::: )   "(" (Set (Var "J")) "," (Set (Var "i")) ")"  ")" )  ($#k8_relset_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "xi")) ($#k1_tarski :::"}"::: ) ))  ($#r1_xboole_0 :::"meets"::: )  (Set (Set  "("  ($#k6_waybel18 :::"proj"::: )   "(" (Set (Var "J")) "," (Set (Var "i")) ")"  ")" )  ($#k8_relset_1 :::"""::: )  (Set (Var "Ai"))))) "holds"  (Bool (Set (Var "xi"))  ($#r2_hidden :::"in"::: )  (Set (Var "Ai")))))))) ; 
 
theorem :: YELLOW17:10 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_waybel18 :::"TopStruct-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I")) "holds"  (Bool (Set (Set  "("  ($#k6_waybel18 :::"proj"::: )   "(" (Set (Var "J")) "," (Set (Var "i")) ")"  ")" )  ($#k8_relset_1 :::"""::: )  (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set  "(" (Set (Var "J"))  ($#k4_waybel18 :::"."::: )  (Set (Var "i")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set  "("  ($#k3_waybel18 :::"product"::: )  (Set (Var "J")) ")" )))))) ; 
 
theorem :: YELLOW17:11 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_waybel18 :::"TopStruct-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I"))  (Bool  "for" (Set (Var "xi")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "J"))  ($#k4_waybel18 :::"."::: )  (Set (Var "i")) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k3_waybel18 :::"product"::: )  (Set (Var "J")) ")" ) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_funct_7 :::"+*"::: )   "(" (Set (Var "i")) "," (Set (Var "xi")) ")" )  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k6_waybel18 :::"proj"::: )   "(" (Set (Var "J")) "," (Set (Var "i")) ")"  ")" )  ($#k8_relset_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "xi")) ($#k1_tarski :::"}"::: ) )))))))) ; 
 
theorem :: YELLOW17:12 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_waybel18 :::"TopStruct-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I"))  (Bool  "for" (Set (Var "xi1")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "J"))  ($#k4_waybel18 :::"."::: )  (Set (Var "i1")) ")" )  (Bool  "for" (Set (Var "Ai2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "J"))  ($#k4_waybel18 :::"."::: )  (Set (Var "i2")) ")" )  "st" (Bool (Bool (Set (Var "Ai2"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set  "(" (Set (Var "J"))  ($#k4_waybel18 :::"."::: )  (Set (Var "i2")) ")" )))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k6_waybel18 :::"proj"::: )   "(" (Set (Var "J")) "," (Set (Var "i1")) ")"  ")" )  ($#k8_relset_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "xi1")) ($#k1_tarski :::"}"::: ) ))  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k6_waybel18 :::"proj"::: )   "(" (Set (Var "J")) "," (Set (Var "i2")) ")"  ")" )  ($#k8_relset_1 :::"""::: )  (Set (Var "Ai2")))) "iff" (Bool  "("  (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set (Var "i2"))) & (Bool (Set (Var "xi1"))  ($#r2_hidden :::"in"::: )  (Set (Var "Ai2")))  ")" )  ")" )))))) ; 
 
theorem :: YELLOW17:13 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_waybel18 :::"TopStruct-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "i1")) "," (Set (Var "i2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I"))  (Bool  "for" (Set (Var "xi1")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "J"))  ($#k4_waybel18 :::"."::: )  (Set (Var "i1")) ")" )  (Bool  "for" (Set (Var "Ai2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "J"))  ($#k4_waybel18 :::"."::: )  (Set (Var "i2")) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k3_waybel18 :::"product"::: )  (Set (Var "J")) ")" )  "st" (Bool (Bool (Set (Var "i1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "i2")))) "holds"  (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k6_waybel18 :::"proj"::: )   "(" (Set (Var "J")) "," (Set (Var "i2")) ")"  ")" )  ($#k8_relset_1 :::"""::: )  (Set (Var "Ai2")))) "iff" (Bool (Set (Set (Var "f"))  ($#k2_funct_7 :::"+*"::: )   "(" (Set (Var "i1")) "," (Set (Var "xi1")) ")" )  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k6_waybel18 :::"proj"::: )   "(" (Set (Var "J")) "," (Set (Var "i2")) ")"  ")" )  ($#k8_relset_1 :::"""::: )  (Set (Var "Ai2"))))  ")" ))))))) ; 
 begin  
theorem :: YELLOW17:14 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_pre_topc :::"TopStruct"::: )   "holds"   (Bool  "("  (Bool (Set (Var "T")) "is"   ($#v1_compts_1 :::"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_tops_2 :::"open"::: )  ) & (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T")))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "F"))))) "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   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T")))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G")))) & (Bool (Set (Var "G")) "is"   ($#v1_finset_1 :::"finite"::: )  )  ")" )))  ")" )) ; 
 
theorem :: YELLOW17:15 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"prebasis":::) "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set (Var "T")) "is"   ($#v1_compts_1 :::"compact"::: )  ) "iff" (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B"))  "st" (Bool (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T")))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "F"))))) "holds"  (Bool  "ex" (Set (Var "G")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "F")) "st" (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T")))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G"))))))  ")" ))) ; 
 begin  
theorem :: YELLOW17:16 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_waybel18 :::"TopStruct-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_waybel18 :::"product_prebasis"::: )  (Set (Var "J"))))) "holds"  (Bool  "ex" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I"))(Bool  "ex" (Set (Var "Ai")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "J"))  ($#k4_waybel18 :::"."::: )  (Set (Var "i")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "Ai")) "is"   ($#v3_pre_topc :::"open"::: )  ) & (Bool (Set (Set  "("  ($#k6_waybel18 :::"proj"::: )   "(" (Set (Var "J")) "," (Set (Var "i")) ")"  ")" )  ($#k8_relset_1 :::"""::: )  (Set (Var "Ai")))  ($#r1_hidden :::"="::: )  (Set (Var "A")))  ")" )))))) ; 
 
theorem :: YELLOW17:17 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_waybel18 :::"TopStruct-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I"))  (Bool  "for" (Set (Var "xi")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "J"))  ($#k4_waybel18 :::"."::: )  (Set (Var "i")) ")" )  (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_waybel18 :::"product_prebasis"::: )  (Set (Var "J")))) & (Bool (Set (Set  "("  ($#k6_waybel18 :::"proj"::: )   "(" (Set (Var "J")) "," (Set (Var "i")) ")"  ")" )  ($#k8_relset_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "xi")) ($#k1_tarski :::"}"::: ) ))  ($#r1_tarski :::"c="::: )  (Set (Var "A"))) & (Bool (Bool  "not" (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set  "("  ($#k3_waybel18 :::"product"::: )  (Set (Var "J")) ")" ))))) "holds"  (Bool  "ex" (Set (Var "Ai")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "J"))  ($#k4_waybel18 :::"."::: )  (Set (Var "i")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "Ai"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set  "(" (Set (Var "J"))  ($#k4_waybel18 :::"."::: )  (Set (Var "i")) ")" ))) & (Bool (Set (Var "xi"))  ($#r2_hidden :::"in"::: )  (Set (Var "Ai"))) & (Bool (Set (Var "Ai")) "is"   ($#v3_pre_topc :::"open"::: )  ) & (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_waybel18 :::"proj"::: )   "(" (Set (Var "J")) "," (Set (Var "i")) ")"  ")" )  ($#k8_relset_1 :::"""::: )  (Set (Var "Ai"))))  ")" ))))))) ; 
 
theorem :: YELLOW17:18 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_waybel18 :::"TopStruct-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I"))  (Bool  "for" (Set (Var "Fi")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "(" (Set (Var "J"))  ($#k4_waybel18 :::"."::: )  (Set (Var "i")) ")" )  "st" (Bool (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set  "(" (Set (Var "J"))  ($#k4_waybel18 :::"."::: )  (Set (Var "i")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "Fi"))))) "holds"  (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set  "("  ($#k3_waybel18 :::"product"::: )  (Set (Var "J")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_tarski :::"union"::: )   "{"  (Set  "(" (Set  "("  ($#k6_waybel18 :::"proj"::: )   "(" (Set (Var "J")) "," (Set (Var "i")) ")"  ")" )  ($#k8_relset_1 :::"""::: )  (Set (Var "Ai")) ")" ) where Ai "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set (Var "Fi")) : (Bool verum)  "}"  )))))) ; 
 
theorem :: YELLOW17:19 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_waybel18 :::"TopStruct-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I"))  (Bool  "for" (Set (Var "xi")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "J"))  ($#k4_waybel18 :::"."::: )  (Set (Var "i")) ")" )  (Bool  "for" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k2_waybel18 :::"product_prebasis"::: )  (Set (Var "J")) ")" )  "st" (Bool (Bool (Set (Set  "("  ($#k6_waybel18 :::"proj"::: )   "(" (Set (Var "J")) "," (Set (Var "i")) ")"  ")" )  ($#k8_relset_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "xi")) ($#k1_tarski :::"}"::: ) ))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G")))) & (Bool  "("   "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_waybel18 :::"product_prebasis"::: )  (Set (Var "J")))) & (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "G")))) "holds"  (Bool  "not" (Bool (Set (Set  "("  ($#k6_waybel18 :::"proj"::: )   "(" (Set (Var "J")) "," (Set (Var "i")) ")"  ")" )  ($#k8_relset_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "xi")) ($#k1_tarski :::"}"::: ) ))  ($#r1_tarski :::"c="::: )  (Set (Var "A"))))  ")" )) "holds"  (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set  "("  ($#k3_waybel18 :::"product"::: )  (Set (Var "J")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G"))))))))) ; 
 
theorem :: YELLOW17:20 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_waybel18 :::"TopStruct-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k2_waybel18 :::"product_prebasis"::: )  (Set (Var "J")) ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "G")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "F"))  "holds" (Bool (Bool  "not" (Set   ($#k2_struct_0 :::"[#]"::: )  (Set  "("  ($#k3_waybel18 :::"product"::: )  (Set (Var "J")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G")))))  ")" )) "holds"  (Bool  "for" (Set (Var "xi")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "J"))  ($#k4_waybel18 :::"."::: )  (Set (Var "i")) ")" )  (Bool  "for" (Set (Var "G")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "F"))  "st" (Bool (Bool (Set (Set  "("  ($#k6_waybel18 :::"proj"::: )   "(" (Set (Var "J")) "," (Set (Var "i")) ")"  ")" )  ($#k8_relset_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "xi")) ($#k1_tarski :::"}"::: ) ))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G"))))) "holds"  (Bool  "ex" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_waybel18 :::"product_prebasis"::: )  (Set (Var "J")))) & (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "G"))) & (Bool (Set (Set  "("  ($#k6_waybel18 :::"proj"::: )   "(" (Set (Var "J")) "," (Set (Var "i")) ")"  ")" )  ($#k8_relset_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "xi")) ($#k1_tarski :::"}"::: ) ))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))  ")" )))))))) ; 
 
theorem :: YELLOW17:21 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_waybel18 :::"TopStruct-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k2_waybel18 :::"product_prebasis"::: )  (Set (Var "J")) ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "G")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "F"))  "holds" (Bool (Bool  "not" (Set   ($#k2_struct_0 :::"[#]"::: )  (Set  "("  ($#k3_waybel18 :::"product"::: )  (Set (Var "J")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G")))))  ")" )) "holds"  (Bool  "for" (Set (Var "xi")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "J"))  ($#k4_waybel18 :::"."::: )  (Set (Var "i")) ")" )  (Bool  "for" (Set (Var "G")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "F"))  "st" (Bool (Bool (Set (Set  "("  ($#k6_waybel18 :::"proj"::: )   "(" (Set (Var "J")) "," (Set (Var "i")) ")"  ")" )  ($#k8_relset_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "xi")) ($#k1_tarski :::"}"::: ) ))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G"))))) "holds"  (Bool  "ex" (Set (Var "Ai")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "J"))  ($#k4_waybel18 :::"."::: )  (Set (Var "i")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "Ai"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set  "(" (Set (Var "J"))  ($#k4_waybel18 :::"."::: )  (Set (Var "i")) ")" ))) & (Bool (Set (Var "xi"))  ($#r2_hidden :::"in"::: )  (Set (Var "Ai"))) & (Bool (Set (Set  "("  ($#k6_waybel18 :::"proj"::: )   "(" (Set (Var "J")) "," (Set (Var "i")) ")"  ")" )  ($#k8_relset_1 :::"""::: )  (Set (Var "Ai")))  ($#r2_hidden :::"in"::: )  (Set (Var "G"))) & (Bool (Set (Var "Ai")) "is"   ($#v3_pre_topc :::"open"::: )  )  ")" )))))))) ; 
 
theorem :: YELLOW17:22 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_waybel18 :::"TopStruct-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k2_waybel18 :::"product_prebasis"::: )  (Set (Var "J")) ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I")) "holds"  (Bool (Set (Set (Var "J"))  ($#k4_waybel18 :::"."::: )  (Set (Var "i"))) "is"   ($#v1_compts_1 :::"compact"::: )  )  ")" ) & (Bool  "("   "for" (Set (Var "G")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "F"))  "holds" (Bool (Bool  "not" (Set   ($#k2_struct_0 :::"[#]"::: )  (Set  "("  ($#k3_waybel18 :::"product"::: )  (Set (Var "J")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G")))))  ")" )) "holds"  (Bool  "ex" (Set (Var "xi")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "J"))  ($#k4_waybel18 :::"."::: )  (Set (Var "i")) ")" ) "st"  (Bool  "for" (Set (Var "G")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "F"))  "holds" (Bool (Bool  "not" (Set (Set  "("  ($#k6_waybel18 :::"proj"::: )   "(" (Set (Var "J")) "," (Set (Var "i")) ")"  ")" )  ($#k8_relset_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "xi")) ($#k1_tarski :::"}"::: ) ))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "G"))))))))))) ; 
 
theorem :: YELLOW17:23 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v4_waybel_3 :::"non-Empty"::: )     ($#v1_waybel18 :::"TopStruct-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I")) "holds"  (Bool (Set (Set (Var "J"))  ($#k4_waybel18 :::"."::: )  (Set (Var "i"))) "is"   ($#v1_compts_1 :::"compact"::: )  )  ")" )) "holds"  (Bool (Set   ($#k3_waybel18 :::"product"::: )  (Set (Var "J"))) "is"   ($#v1_compts_1 :::"compact"::: )  ))) ;