take TOP-REAL n ; :: thesis: TOP-REAL n is n -locally_euclidean
thus TOP-REAL n is n -locally_euclidean ; :: thesis: verum