:: deftheorem defines the_Complex_Space COMPLSP1:def 1 :
for n being Element of NAT holds the_Complex_Space n = TopStruct(# (COMPLEX n),(ComplexOpenSets n) #);