theorem :: COMPLSP1:1

for n being Element of NAT holds the topology of (the_Complex_Space n) = ComplexOpenSets n ;