let M be non empty compact locally_euclidean TopSpace; :: thesis: ( M is connected implies ex n being Nat st M is n -locally_euclidean )
A1: for A being Subset of M st A is connected & [#] M c= A holds
A = [#] M ;
assume M is connected ; :: thesis: ex n being Nat st M is n -locally_euclidean
then [#] M is a_component by A1, CONNSP_1:27, CONNSP_1:def 5;
then consider n being Nat such that
A2: M | ([#] M) is non empty n -locally_euclidean TopSpace by Th14;
M | ([#] M),M are_homeomorphic by Th1;
then M is n -locally_euclidean by Th11, A2;
hence ex n being Nat st M is n -locally_euclidean ; :: thesis: verum