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