theorem :: FINTOPO8:44

for T being non empty TopSpace
for O being open Subset of T holds O is open Subset of (Top2NTop T) by Lm1;