take M = Tdisk ((0. (TOP-REAL n)),1); :: thesis: M is n -locally_euclidean
thus M is n -locally_euclidean ; :: thesis: verum