let T be non empty TopSpace; :: thesis: ( T is first-countable implies for x being Point of T ex B being Basis of x ex S being Function st
( dom S = NAT & rng S = B & ( for n, m being Element of NAT st m >= n holds
S . m c= S . n ) ) )
assume A1: T is first-countable ; :: thesis: for x being Point of T ex B being Basis of x ex S being Function st
( dom S = NAT & rng S = B & ( for n, m being Element of NAT st m >= n holds
S . m c= S . n ) )
let x be Point of T; :: thesis: ex B being Basis of x ex S being Function st
( dom S = NAT & rng S = B & ( for n, m being Element of NAT st m >= n holds
S . m c= S . n ) )
consider B1 being Basis of x such that
A2: B1 is countable by A1, FRECHET:def 2;
consider f being Function of NAT,B1 such that
A3: rng f = B1 by A2, CARD_3:96;
defpred S₁[ set , set ] means $2 = meet (f .: (succ $1));
A4: for n being set st n in NAT holds
ex A being set st S₁[n,A] ;
consider S being Function such that
A5: dom S = NAT and
A6: for n being set st n in NAT holds
S₁[n,S . n] from CLASSES1:sch 1(A4);
A7: rng S c= bool the carrier of T

proof

let A be set ; :: according to TARSKI:def 3 :: thesis: ( not A in rng S or A in bool the carrier of T )
assume A in rng S ; :: thesis: A in bool the carrier of T
then consider n being set such that
A8: ( n in dom S & A = S . n ) by FUNCT_1:def 3;
reconsider fsuccn = f .: (succ n) as Subset-Family of T by XBOOLE_1:1;
meet fsuccn = meet (f .: (succ n)) ;
then meet (f .: (succ n)) in bool the carrier of T ;
hence A in bool the carrier of T by A5, A6, A8; :: thesis: verum

end;

then reconsider B = rng S as Subset-Family of T ;
reconsider B = B as Subset-Family of T ;
A9: ex A being set st A in B

proof

take A = meet (f .: (succ 0)); :: thesis: A in B
A = S . 0 by A6;
hence A in B by A5, FUNCT_1:def 3; :: thesis: verum

end;

then A10: Intersect B = meet B by SETFAM_1:def 9;
for A being set st A in B holds
x in A

proof

let A be set ; :: thesis: ( A in B implies x in A )
assume A in B ; :: thesis: x in A
then consider n being set such that
A11: n in dom S and
A12: A = S . n by FUNCT_1:def 3;
( dom f = NAT & n in succ n ) by FUNCT_2:def 1, ORDINAL1:6;
then A13: f . n in f .: (succ n) by A5, A11, FUNCT_1:def 6;
A14: for A1 being set st A1 in f .: (succ n) holds
x in A1

proof

let A1 be set ; :: thesis: ( A1 in f .: (succ n) implies x in A1 )
assume A1 in f .: (succ n) ; :: thesis: x in A1
then consider m being set such that
A15: m in dom f and
m in succ n and
A16: A1 = f . m by FUNCT_1:def 6;
f . m in rng f by A15, FUNCT_1:def 3;
then reconsider A2 = A1 as Subset of T by A3, A16;
reconsider A2 = A2 as Subset of T ;
A2 in B1 by A3, A15, A16, FUNCT_1:def 3;
hence x in A1 by YELLOW_8:12; :: thesis: verum

end;

A = meet (f .: (succ n)) by A5, A6, A11, A12;
hence x in A by A14, A13, SETFAM_1:def 1; :: thesis: verum

end;

then A17: x in meet B by A9, SETFAM_1:def 1;
A18: B c= the topology of T

proof

let A be set ; :: according to TARSKI:def 3 :: thesis: ( not A in B or A in the topology of T )
assume A in B ; :: thesis: A in the topology of T
then consider n being set such that
A19: n in dom S and
A20: A = S . n by FUNCT_1:def 3;
reconsider n9 = n as Element of NAT by A5, A19;
reconsider C = f .: (succ n) as Subset-Family of T by XBOOLE_1:1;
A21: C is open

proof

let P be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( not P in C or P is open )
assume P in C ; :: thesis: P is open
hence P is open by YELLOW_8:12; :: thesis: verum

end;

succ n9 is finite ;
then f .: (succ n) is finite ;
then A22: meet C is open by A21, TOPS_2:20;
A = meet (f .: (succ n)) by A5, A6, A19, A20;
hence A in the topology of T by A22, PRE_TOPC:def 2; :: thesis: verum

end;

for O being Subset of T st O is open & x in O holds
ex A being Subset of T st
( A in B & A c= O )

proof

let O be Subset of T; :: thesis: ( O is open & x in O implies ex A being Subset of T st
( A in B & A c= O ) )
assume ( O is open & x in O ) ; :: thesis: ex A being Subset of T st
( A in B & A c= O )
then consider A1 being Subset of T such that
A23: A1 in B1 and
A24: A1 c= O by YELLOW_8:def 1;
consider n being set such that
A25: n in dom f and
A26: A1 = f . n by A3, A23, FUNCT_1:def 3;
S . n in rng S by A5, A25, FUNCT_1:def 3;
then reconsider A = S . n as Subset of T by A7;
reconsider A = A as Subset of T ;
take A ; :: thesis: ( A in B & A c= O )
thus A in B by A5, A25, FUNCT_1:def 3; :: thesis: A c= O
n in succ n by ORDINAL1:6;
then f . n in f .: (succ n) by A25, FUNCT_1:def 6;
then meet (f .: (succ n)) c= A1 by A26, SETFAM_1:3;
then S . n c= A1 by A6, A25;
hence A c= O by A24, XBOOLE_1:1; :: thesis: verum

end;

then reconsider B = B as Basis of x by A18, A10, A17, TOPS_2:64, YELLOW_8:def 1;
take B ; :: thesis: ex S being Function st
( dom S = NAT & rng S = B & ( for n, m being Element of NAT st m >= n holds
S . m c= S . n ) )
take S ; :: thesis: ( dom S = NAT & rng S = B & ( for n, m being Element of NAT st m >= n holds
S . m c= S . n ) )
thus dom S = NAT by A5; :: thesis: ( rng S = B & ( for n, m being Element of NAT st m >= n holds
S . m c= S . n ) )
thus rng S = B ; :: thesis: for n, m being Element of NAT st m >= n holds
S . m c= S . n
for n, m being Element of NAT st m >= n holds
S . m c= S . n

proof

let n, m be Element of NAT ; :: thesis: ( m >= n implies S . m c= S . n )
assume m >= n ; :: thesis: S . m c= S . n
then n + 1 <= m + 1 by XREAL_1:6;
then n + 1 c= m + 1 by NAT_1:39;
then succ n c= m + 1 by NAT_1:38;
then succ n c= succ m by NAT_1:38;
then A27: f .: (succ n) c= f .: (succ m) by RELAT_1:123;
( 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;
then meet (f .: (succ m)) c= meet (f .: (succ n)) by A27, SETFAM_1:6;
then S . m c= meet (f .: (succ n)) by A6;
hence S . m c= S . n by A6; :: thesis: verum

end;

hence for n, m being Element of NAT st m >= n holds
S . m c= S . n ; :: thesis: verum