theorem :: FINTOPO8:3

for NT being NTopSpace
for O being open Subset of NT holds O is open Subset of (NTop2Top NT) by Lm9;