:: deftheorem defines Top2NTop FINTOPO8:def 17 :
for T being non empty TopSpace
for S being Subset of T holds Top2NTop S = S;