:: COMPLSP1  semantic presentation begin  





definitionlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); func  :::"the_Complex_Space"::: "n" ->   ($#v1_pre_topc :::"strict"::: )    ($#l1_pre_topc :::"TopSpace":::) equals :: COMPLSP1:def 1 (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "("  ($#k14_seq_4 :::"COMPLEX"::: )  "n" ")" ) "," (Set  "("  ($#k27_seq_4 :::"ComplexOpenSets"::: )  "n" ")" ) "#)" ); end; 





:: deftheorem    defines :::"the_Complex_Space"::: COMPLSP1:def 1 :  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k1_complsp1 :::"the_Complex_Space"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "("  ($#k14_seq_4 :::"COMPLEX"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k27_seq_4 :::"ComplexOpenSets"::: )  (Set (Var "n")) ")" ) "#)" ))); 
 registrationlet "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set   ($#k1_complsp1 :::"the_Complex_Space"::: )  "n") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_pre_topc :::"strict"::: )   ; 
end; 
theorem :: COMPLSP1:1 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set  "("  ($#k1_complsp1 :::"the_Complex_Space"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k27_seq_4 :::"ComplexOpenSets"::: )  (Set (Var "n"))))) ; 
 
theorem :: COMPLSP1:2 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k1_complsp1 :::"the_Complex_Space"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k14_seq_4 :::"COMPLEX"::: )  (Set (Var "n"))))) ; 
 







theorem :: COMPLSP1:3 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k1_complsp1 :::"the_Complex_Space"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set (Var "p")) "is"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set   ($#k14_seq_4 :::"COMPLEX"::: )  (Set (Var "n")))))) ; 
 
theorem :: COMPLSP1:4 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_complsp1 :::"the_Complex_Space"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k14_seq_4 :::"COMPLEX"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "V")))) "holds"  (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v1_seq_4 :::"open"::: )  ) "iff" (Bool (Set (Var "V")) "is"   ($#v3_pre_topc :::"open"::: )  )  ")" )))) ; 
 
theorem :: COMPLSP1:5 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_complsp1 :::"the_Complex_Space"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k14_seq_4 :::"COMPLEX"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "V")))) "holds"  (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v2_seq_4 :::"closed"::: )  ) "iff" (Bool (Set (Var "V")) "is"   ($#v4_pre_topc :::"closed"::: )  )  ")" )))) ; 
 
theorem :: COMPLSP1:6 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k1_complsp1 :::"the_Complex_Space"::: )  (Set (Var "n"))) "is"   ($#v8_pre_topc :::"T_2"::: )  )) ; 
 
theorem :: COMPLSP1:7 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k1_complsp1 :::"the_Complex_Space"::: )  (Set (Var "n"))) "is"   ($#v9_pre_topc :::"regular"::: )  )) ;