theorem :: FINTOPO8:5

for NT being NTopSpace holds
( [#] NT is open & {} NT is open ) ;