take TOP-REAL n ; :: thesis: ( TOP-REAL n is second-countable & TOP-REAL n is Hausdorff & TOP-REAL n is n -locally_euclidean )
thus ( TOP-REAL n is second-countable & TOP-REAL n is Hausdorff & TOP-REAL n is n -locally_euclidean ) ; :: thesis: verum