let T be non empty TopSpace; :: thesis: ( T is first-countable implies T is Frechet )

assume A1: T is first-countable ; :: thesis: T is Frechet

let A be Subset of T; :: according to FRECHET:def 6 :: thesis: for x being Point of T st x in Cl A holds

ex S being sequence of T st

( rng S c= A & x in Lim S )

let x be Point of T; :: thesis: ( x in Cl A implies ex S being sequence of T st

( rng S c= A & x in Lim S ) )

assume A2: x in Cl A ; :: thesis: ex S being sequence of T st

( rng S c= A & x in Lim S )

consider B being Basis of x such that

A3: B is countable by A1;

consider f being sequence of B such that

A4: rng f = B by A3, CARD_3:96;

defpred S_{1}[ object , object ] means ex D1 being set st

( D1 = $1 & $2 in A /\ (meet (f .: (succ D1))) );

A5: for n being object st n in NAT holds

ex y being object st

( y in the carrier of T & S_{1}[n,y] )

A21: ( dom S = NAT & rng S c= the carrier of T & ( for n being object st n in NAT holds

S_{1}[n,S . n] ) )
from FUNCT_1:sch 6(A5);

A22: rng S c= A

A24: for m, n being Nat st n <= m holds

A /\ (meet (f .: (succ m))) c= A /\ (meet (f .: (succ n)))

hence ex S being sequence of T st

( rng S c= A & x in Lim S ) by A22; :: thesis: verum

assume A1: T is first-countable ; :: thesis: T is Frechet

let A be Subset of T; :: according to FRECHET:def 6 :: thesis: for x being Point of T st x in Cl A holds

ex S being sequence of T st

( rng S c= A & x in Lim S )

let x be Point of T; :: thesis: ( x in Cl A implies ex S being sequence of T st

( rng S c= A & x in Lim S ) )

assume A2: x in Cl A ; :: thesis: ex S being sequence of T st

( rng S c= A & x in Lim S )

consider B being Basis of x such that

A3: B is countable by A1;

consider f being sequence of B such that

A4: rng f = B by A3, CARD_3:96;

defpred S

( D1 = $1 & $2 in A /\ (meet (f .: (succ D1))) );

A5: for n being object st n in NAT holds

ex y being object st

( y in the carrier of T & S

proof

consider S being Function such that
defpred S_{2}[ Nat] means ex H being Subset of T st

( H = meet (f .: (succ $1)) & H is open );

let n be object ; :: thesis: ( n in NAT implies ex y being object st

( y in the carrier of T & S_{1}[n,y] ) )

A6: for n being Nat st S_{2}[n] holds

S_{2}[n + 1]

( y in the carrier of T & S_{1}[n,y] )

then reconsider n = n as Element of NAT ;

A15: S_{2}[ 0 ]
_{2}[n]
from NAT_1:sch 2(A15, A6);

then A16: ex H being Subset of T st

( H = meet (f .: (succ n)) & H is open ) ;

A17: for G being set st G in f .: (succ n) holds

x in G

then f . n in f .: (succ n) by FUNCT_1:def 6;

then x in meet (f .: (succ n)) by A17, SETFAM_1:def 1;

then A meets meet (f .: (succ n)) by A2, A16, PRE_TOPC:def 7;

then consider y being object such that

A20: y in A /\ (meet (f .: (succ n))) by XBOOLE_0:4;

take y ; :: thesis: ( y in the carrier of T & S_{1}[n,y] )

thus ( y in the carrier of T & S_{1}[n,y] )
by A20; :: thesis: verum

end;( H = meet (f .: (succ $1)) & H is open );

let n be object ; :: thesis: ( n in NAT implies ex y being object st

( y in the carrier of T & S

A6: for n being Nat st S

S

proof

assume
n in NAT
; :: thesis: ex y being object st
let n be Nat; :: thesis: ( S_{2}[n] implies S_{2}[n + 1] )

given G being Subset of T such that A7: G = meet (f .: (succ n)) and

A8: G is open ; :: thesis: S_{2}[n + 1]

n + 1 in NAT ;

then A9: n + 1 in dom f by FUNCT_2:def 1;

A10: n in NAT by ORDINAL1:def 12;

( n in succ n & dom f = NAT ) by FUNCT_2:def 1, ORDINAL1:6;

then A11: f . n in f .: (succ n) by FUNCT_1:def 6, A10;

f . (n + 1) in B ;

then consider H1 being Subset of T such that

A12: H1 = f . (n + 1) ;

A13: H1 is open by A12, YELLOW_8:12;

consider H being Subset of T such that

A14: H = H1 /\ G ;

take H ; :: thesis: ( H = meet (f .: (succ (n + 1))) & H is open )

meet (f .: (succ (n + 1))) = meet (f .: ({(n + 1)} \/ (Segm (n + 1))))

.= meet (f .: ({(n + 1)} \/ (succ (Segm n)))) by NAT_1:38

.= meet ((Im (f,(n + 1))) \/ (f .: (succ n))) by RELAT_1:120

.= meet ({(f . (n + 1))} \/ (f .: (succ n))) by A9, FUNCT_1:59

.= (meet {(f . (n + 1))}) /\ (meet (f .: (succ n))) by A11, SETFAM_1:9

.= H by A7, A12, A14, SETFAM_1:10 ;

hence ( H = meet (f .: (succ (n + 1))) & H is open ) by A8, A13, A14, TOPS_1:11; :: thesis: verum

end;given G being Subset of T such that A7: G = meet (f .: (succ n)) and

A8: G is open ; :: thesis: S

n + 1 in NAT ;

then A9: n + 1 in dom f by FUNCT_2:def 1;

A10: n in NAT by ORDINAL1:def 12;

( n in succ n & dom f = NAT ) by FUNCT_2:def 1, ORDINAL1:6;

then A11: f . n in f .: (succ n) by FUNCT_1:def 6, A10;

f . (n + 1) in B ;

then consider H1 being Subset of T such that

A12: H1 = f . (n + 1) ;

A13: H1 is open by A12, YELLOW_8:12;

consider H being Subset of T such that

A14: H = H1 /\ G ;

take H ; :: thesis: ( H = meet (f .: (succ (n + 1))) & H is open )

meet (f .: (succ (n + 1))) = meet (f .: ({(n + 1)} \/ (Segm (n + 1))))

.= meet (f .: ({(n + 1)} \/ (succ (Segm n)))) by NAT_1:38

.= meet ((Im (f,(n + 1))) \/ (f .: (succ n))) by RELAT_1:120

.= meet ({(f . (n + 1))} \/ (f .: (succ n))) by A9, FUNCT_1:59

.= (meet {(f . (n + 1))}) /\ (meet (f .: (succ n))) by A11, SETFAM_1:9

.= H by A7, A12, A14, SETFAM_1:10 ;

hence ( H = meet (f .: (succ (n + 1))) & H is open ) by A8, A13, A14, TOPS_1:11; :: thesis: verum

( y in the carrier of T & S

then reconsider n = n as Element of NAT ;

A15: S

proof

for n being Nat holds S
f . 0 in B
;

then reconsider H = f . 0 as Subset of T ;

take H ; :: thesis: ( H = meet (f .: (succ 0)) & H is open )

0 in NAT ;

then 0 in dom f by FUNCT_2:def 1;

then meet (Im (f,0)) = meet {(f . 0)} by FUNCT_1:59

.= H by SETFAM_1:10 ;

hence ( H = meet (f .: (succ 0)) & H is open ) by YELLOW_8:12; :: thesis: verum

end;then reconsider H = f . 0 as Subset of T ;

take H ; :: thesis: ( H = meet (f .: (succ 0)) & H is open )

0 in NAT ;

then 0 in dom f by FUNCT_2:def 1;

then meet (Im (f,0)) = meet {(f . 0)} by FUNCT_1:59

.= H by SETFAM_1:10 ;

hence ( H = meet (f .: (succ 0)) & H is open ) by YELLOW_8:12; :: thesis: verum

then A16: ex H being Subset of T st

( H = meet (f .: (succ n)) & H is open ) ;

A17: for G being set st G in f .: (succ n) holds

x in G

proof

( n in succ n & dom f = NAT )
by FUNCT_2:def 1, ORDINAL1:6;
let G be set ; :: thesis: ( G in f .: (succ n) implies x in G )

assume G in f .: (succ n) ; :: thesis: x in G

then consider k being object such that

A18: k in dom f and

k in succ n and

A19: G = f . k by FUNCT_1:def 6;

f . k in B by A18, FUNCT_2:5;

hence x in G by A19, YELLOW_8:12; :: thesis: verum

end;assume G in f .: (succ n) ; :: thesis: x in G

then consider k being object such that

A18: k in dom f and

k in succ n and

A19: G = f . k by FUNCT_1:def 6;

f . k in B by A18, FUNCT_2:5;

hence x in G by A19, YELLOW_8:12; :: thesis: verum

then f . n in f .: (succ n) by FUNCT_1:def 6;

then x in meet (f .: (succ n)) by A17, SETFAM_1:def 1;

then A meets meet (f .: (succ n)) by A2, A16, PRE_TOPC:def 7;

then consider y being object such that

A20: y in A /\ (meet (f .: (succ n))) by XBOOLE_0:4;

take y ; :: thesis: ( y in the carrier of T & S

thus ( y in the carrier of T & S

A21: ( dom S = NAT & rng S c= the carrier of T & ( for n being object st n in NAT holds

S

A22: rng S c= A

proof

reconsider S = S as sequence of T by A21, FUNCT_2:def 1, RELSET_1:4;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng S or y in A )

assume y in rng S ; :: thesis: y in A

then consider a being object such that

A23: ( a in dom S & y = S . a ) by FUNCT_1:def 3;

reconsider a = a as set by TARSKI:1;

S_{1}[a,S . a]
by A21, A23;

then y in A /\ (meet (f .: (succ a))) by A23;

hence y in A by XBOOLE_0:def 4; :: thesis: verum

end;assume y in rng S ; :: thesis: y in A

then consider a being object such that

A23: ( a in dom S & y = S . a ) by FUNCT_1:def 3;

reconsider a = a as set by TARSKI:1;

S

then y in A /\ (meet (f .: (succ a))) by A23;

hence y in A by XBOOLE_0:def 4; :: thesis: verum

A24: for m, n being Nat st n <= m holds

A /\ (meet (f .: (succ m))) c= A /\ (meet (f .: (succ n)))

proof

S is_convergent_to x
let m, n be Nat; :: thesis: ( n <= m implies A /\ (meet (f .: (succ m))) c= A /\ (meet (f .: (succ n))) )

assume n <= m ; :: thesis: A /\ (meet (f .: (succ m))) c= A /\ (meet (f .: (succ n)))

then n + 1 <= m + 1 by XREAL_1:6;

then Segm (n + 1) c= Segm (m + 1) by NAT_1:39;

then succ (Segm n) c= Segm (m + 1) by NAT_1:38;

then succ (Segm n) c= succ (Segm m) by NAT_1:38;

then A25: f .: (succ n) c= f .: (succ m) by RELAT_1:123;

A26: n in NAT by ORDINAL1:def 12;

( n in succ n & dom f = NAT ) by FUNCT_2:def 1, ORDINAL1:6;

then f . n in f .: (succ n) by FUNCT_1:def 6, A26;

then meet (f .: (succ m)) c= meet (f .: (succ n)) by A25, SETFAM_1:6;

hence A /\ (meet (f .: (succ m))) c= A /\ (meet (f .: (succ n))) by XBOOLE_1:26; :: thesis: verum

end;assume n <= m ; :: thesis: A /\ (meet (f .: (succ m))) c= A /\ (meet (f .: (succ n)))

then n + 1 <= m + 1 by XREAL_1:6;

then Segm (n + 1) c= Segm (m + 1) by NAT_1:39;

then succ (Segm n) c= Segm (m + 1) by NAT_1:38;

then succ (Segm n) c= succ (Segm m) by NAT_1:38;

then A25: f .: (succ n) c= f .: (succ m) by RELAT_1:123;

A26: n in NAT by ORDINAL1:def 12;

( n in succ n & dom f = NAT ) by FUNCT_2:def 1, ORDINAL1:6;

then f . n in f .: (succ n) by FUNCT_1:def 6, A26;

then meet (f .: (succ m)) c= meet (f .: (succ n)) by A25, SETFAM_1:6;

hence A /\ (meet (f .: (succ m))) c= A /\ (meet (f .: (succ n))) by XBOOLE_1:26; :: thesis: verum

proof

then
x in Lim S
by Def5;
let U1 be Subset of T; :: according to FRECHET:def 3 :: thesis: ( U1 is open & x in U1 implies ex n being Nat st

for m being Nat st n <= m holds

S . m in U1 )

assume A27: ( U1 is open & x in U1 ) ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

S . m in U1

reconsider U1 = U1 as Subset of T ;

consider U2 being Subset of T such that

A28: U2 in B and

A29: U2 c= U1 by A27, YELLOW_8:13;

consider n being object such that

A30: n in dom f and

A31: U2 = f . n by A4, A28, FUNCT_1:def 3;

reconsider n = n as Element of NAT by A30;

for m being Nat st n <= m holds

S . m in U1

for m being Nat st n <= m holds

S . m in U1 ; :: thesis: verum

end;for m being Nat st n <= m holds

S . m in U1 )

assume A27: ( U1 is open & x in U1 ) ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

S . m in U1

reconsider U1 = U1 as Subset of T ;

consider U2 being Subset of T such that

A28: U2 in B and

A29: U2 c= U1 by A27, YELLOW_8:13;

consider n being object such that

A30: n in dom f and

A31: U2 = f . n by A4, A28, FUNCT_1:def 3;

reconsider n = n as Element of NAT by A30;

for m being Nat st n <= m holds

S . m in U1

proof

hence
ex n being Nat st
let m be Nat; :: thesis: ( n <= m implies S . m in U1 )

A32: m in NAT by ORDINAL1:def 12;

( n in succ n & dom f = NAT ) by FUNCT_2:def 1, ORDINAL1:6;

then A33: f . n in f .: (succ n) by FUNCT_1:def 6;

assume n <= m ; :: thesis: S . m in U1

then A34: A /\ (meet (f .: (succ m))) c= A /\ (meet (f .: (succ n))) by A24;

S_{1}[m,S . m]
by A21, A32;

then S . m in A /\ (meet (f .: (succ m))) ;

then S . m in meet (f .: (succ n)) by A34, XBOOLE_0:def 4;

then S . m in f . n by A33, SETFAM_1:def 1;

hence S . m in U1 by A29, A31; :: thesis: verum

end;A32: m in NAT by ORDINAL1:def 12;

( n in succ n & dom f = NAT ) by FUNCT_2:def 1, ORDINAL1:6;

then A33: f . n in f .: (succ n) by FUNCT_1:def 6;

assume n <= m ; :: thesis: S . m in U1

then A34: A /\ (meet (f .: (succ m))) c= A /\ (meet (f .: (succ n))) by A24;

S

then S . m in A /\ (meet (f .: (succ m))) ;

then S . m in meet (f .: (succ n)) by A34, XBOOLE_0:def 4;

then S . m in f . n by A33, SETFAM_1:def 1;

hence S . m in U1 by A29, A31; :: thesis: verum

for m being Nat st n <= m holds

S . m in U1 ; :: thesis: verum

hence ex S being sequence of T st

( rng S c= A & x in Lim S ) by A22; :: thesis: verum