let M be non empty TopSpace; :: thesis: ( M is without_boundary & M is locally_euclidean implies M is first-countable )
assume A1: ( M is without_boundary & M is locally_euclidean ) ; :: thesis:
for p being Point of M ex B being Basis of p st B is countable
proof
let p be Point of M; :: thesis: ex B being Basis of p st B is countable
consider U being a_neighborhood of p, n being Nat such that
A2: M | U, Tball ((0. ()),1) are_homeomorphic by ;
set TR = TOP-REAL n;
p in Int U by CONNSP_2:def 1;
then K1: ex W being Subset of M st
( W is open & W c= U & p in W ) by TOPS_1:22;
( not Ball ((0. ()),1) is empty & Ball ((0. ()),1) is ball ) ;
then Tball ((0. ()),1),() | ([#] ()) are_homeomorphic by ;
then M | U,() | ([#] ()) are_homeomorphic by ;
then M | U, TopStruct(# the carrier of (), the topology of () #) are_homeomorphic by TSEP_1:93;
then consider f being Function of (M | U),TopStruct(# the carrier of (), the topology of () #) such that
A3: f is being_homeomorphism by T_0TOPSP:def 1;
A4: ( dom f = [#] (M | U) & rng f = [#] TopStruct(# the carrier of (), the topology of () #) & f is one-to-one & f is continuous & f " is continuous ) by ;
then A5: dom f = U by PRE_TOPC:def 5;
A6: f is onto by ;
A7: Int U c= U by TOPS_1:16;
A8: p in Int U by CONNSP_2:def 1;
A9: p in dom f by ;
f . p in rng f by ;
then reconsider q = f . p as Point of () ;
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
consider B1 being Basis of q such that
A10: B1 is countable by FRECHET:def 2;
reconsider A = bool the carrier of () as non empty set ;
deffunc H1( set ) -> Element of bool the carrier of M = ((f ") .: c1) /\ (Int U);
set B = { H1(X) where X is Element of A : X in B1 } ;
A11: card B1 c= omega by ;
card { H1(X) where X is Element of A : X in B1 } c= card B1 from then A12: card { H1(X) where X is Element of A : X in B1 } c= omega by A11;
for x being object st x in { H1(X) where X is Element of A : X in B1 } holds
x in bool the carrier of M
proof
let x be object ; :: thesis: ( x in { H1(X) where X is Element of A : X in B1 } implies x in bool the carrier of M )
assume x in { H1(X) where X is Element of A : X in B1 } ; :: thesis: x in bool the carrier of M
then consider X1 being Element of A such that
A13: ( x = H1(X1) & X1 in B1 ) ;
thus x in bool the carrier of M by A13; :: thesis: verum
end;
then reconsider B = { H1(X) where X is Element of A : X in B1 } as Subset-Family of M by TARSKI:def 3;
A14: for P being Subset of M st P in B holds
P is open
proof
let P be Subset of M; :: thesis: ( P in B implies P is open )
assume P in B ; :: thesis: P is open
then consider X1 being Element of A such that
A15: ( P = H1(X1) & X1 in B1 ) ;
reconsider X1 = X1 as Subset of TopStruct(# the carrier of (), the topology of () #) ;
reconsider X2 = X1 as Subset of () ;
X2 in the topology of () by ;
then A16: X1 is open by PRE_TOPC:def 2;
reconsider U1 = M | U as non empty TopStruct by A8, A7;
reconsider g = f " as Function of TopStruct(# the carrier of (), the topology of () #),U1 ;
A17: g is being_homeomorphism by ;
A18: g .: X1 is open by ;
g .: X1 in the topology of (M | U) by ;
then consider Q being Subset of M such that
A19: ( Q in the topology of M & g .: X1 = Q /\ ([#] (M | U)) ) by PRE_TOPC:def 4;
[#] (M | U) = U by PRE_TOPC:def 5;
then A20: P = Q /\ (U /\ (Int U)) by
.= Q /\ (Int U) by ;
Q is open by ;
hence P is open by A20; :: thesis: verum
end;
for Y being set st Y in B holds
p in Y
proof
let Y be set ; :: thesis: ( Y in B implies p in Y )
assume Y in B ; :: thesis: p in Y
then consider X1 being Element of A such that
A21: ( Y = H1(X1) & X1 in B1 ) ;
reconsider g = f as Function ;
[p,(g . p)] in g by ;
then [q,p] in g ~ by RELAT_1:def 7;
then [q,p] in g " by ;
then A22: [q,p] in f " by ;
q in X1 by ;
then p in (f ") .: X1 by ;
hence p in Y by ; :: thesis: verum
end;
then A23: p in Intersect B by SETFAM_1:43;
for S being Subset of M st S is open & p in S holds
ex V being Subset of M st
( V in B & V c= S )
proof
let S be Subset of M; :: thesis: ( S is open & p in S implies ex V being Subset of M st
( V in B & V c= S ) )

assume A24: ( S is open & p in S ) ; :: thesis: ex V being Subset of M st
( V in B & V c= S )

set S1 = S /\ ([#] (M | U));
S in the topology of M by ;
then A25: S /\ ([#] (M | U)) in the topology of (M | U) by PRE_TOPC:def 4;
reconsider U1 = M | U as non empty TopStruct by A8, A7;
reconsider S1 = S /\ ([#] (M | U)) as Subset of U1 ;
S1 is open by ;
then A26: f .: S1 is open by ;
reconsider S2 = f .: S1 as Subset of () ;
K: f .: S1 in the topology of TopStruct(# the carrier of (), the topology of () #) by ;
reconsider g1 = f as Function ;
A28: [p,q] in f by ;
p in S1 by ;
then A29: q in S2 by ;
consider W being Subset of () such that
A30: ( W in B1 & W c= S2 ) by ;
reconsider W = W as Element of A ;
set V = ((f ") .: W) /\ (Int U);
reconsider V = ((f ") .: W) /\ (Int U) as Subset of M ;
take V ; :: thesis: ( V in B & V c= S )
thus V in B by A30; :: thesis: V c= S
A31: g1 " = f " by ;
A32: (f ") .: (f .: S1) = S1 by ;
A33: ((f ") .: W) /\ (Int U) c= (f ") .: W by XBOOLE_1:17;
A34: S1 c= S by XBOOLE_1:17;
(f ") .: W c= (f ") .: (f .: S1) by ;
hence V c= S by ; :: thesis: verum
end;
then reconsider B = B as Basis of p by ;
take B ; :: thesis: B is countable
thus B is countable by ; :: thesis: verum
end;
hence M is first-countable by FRECHET:def 2; :: thesis: verum