take T = Tdisk ((0. (TOP-REAL n)),1); :: thesis: ( T is second-countable & T is Hausdorff & T is n -locally_euclidean )
thus ( T is second-countable & T is Hausdorff & T is n -locally_euclidean ) ; :: thesis: verum