theorem :: FINTOPO8:43

for T being non empty TopSpace
for F being closed Subset of T holds F is closed Subset of (Top2NTop T) by Lm7;