for T being non empty T_2 TopSpace holds Top2NTop T is T_2 NTopSpace by Lm28;