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 1;
consider f being Function of NAT ,B1 such that
A3: rng f = B1 by A2, CARD_3:146;
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: 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 A8: m >= n ; :: thesis: S . m c= S . n
( n in succ n & dom f = NAT ) by FUNCT_2:def 1, ORDINAL1:10;
then A9: f . n in f .: (succ n) by FUNCT_1:def 12;
n + 1 <= m + 1 by A8, XREAL_1:8;
then n + 1 c= m + 1 by NAT_1:40;
then succ n c= m + 1 by NAT_1:39;
then succ n c= succ m by NAT_1:39;
then f .: (succ n) c= f .: (succ m) by RELAT_1:156;
then meet (f .: (succ m)) c= meet (f .: (succ n)) by A9, SETFAM_1:7;
then S . m c= meet (f .: (succ n)) by A6;
hence S . m c= S . n by A6; :: thesis: verum

end;

A10: 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
A11: n in dom S and
A12: A = S . n by FUNCT_1:def 5;
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, A11, A12; :: thesis: verum

end;

then reconsider B = rng S as Subset-Family of T ;
reconsider B = B as Subset-Family of T ;
A13: 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
A14: n in dom S and
A15: A = S . n by FUNCT_1:def 5;
A16: A = meet (f .: (succ n)) by A5, A6, A14, A15;
reconsider C = f .: (succ n) as Subset-Family of T by XBOOLE_1:1;
reconsider n' = n as Element of NAT by A5, A14;
succ n' is finite ;
then A17: f .: (succ n) is finite by FINSET_1:17;
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:21; :: thesis: verum

end;

then meet C is open by A17, TOPS_2:27;
hence A in the topology of T by A16, PRE_TOPC:def 5; :: thesis: verum

end;

A18: 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 5; :: thesis: verum

end;

then A19: Intersect B = meet B by SETFAM_1:def 10;
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
A20: n in dom S and
A21: A = S . n by FUNCT_1:def 5;
A22: A = meet (f .: (succ n)) by A5, A6, A20, A21;
A23: 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
A24: m in dom f and
m in succ n and
A25: A1 = f . m by FUNCT_1:def 12;
f . m in rng f by A24, FUNCT_1:def 5;
then reconsider A2 = A1 as Subset of T by A3, A25;
reconsider A2 = A2 as Subset of T ;
A2 in B1 by A3, A24, A25, FUNCT_1:def 5;
hence x in A1 by YELLOW_8:21; :: thesis: verum

end;

A26: dom f = NAT by FUNCT_2:def 1;
n in succ n by ORDINAL1:10;
then f . n in f .: (succ n) by A5, A20, A26, FUNCT_1:def 12;
hence x in A by A22, A23, SETFAM_1:def 1; :: thesis: verum

end;

then A27: x in meet B by A18, SETFAM_1:def 1;
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
A28: A1 in B1 and
A29: A1 c= O by YELLOW_8:def 2;
consider n being set such that
A30: n in dom f and
A31: A1 = f . n by A3, A28, FUNCT_1:def 5;
S . n in rng S by A5, A30, FUNCT_1:def 5;
then reconsider A = S . n as Subset of T by A10;
reconsider A = A as Subset of T ;
take A ; :: thesis: ( A in B & A c= O )
thus A in B by A5, A30, FUNCT_1:def 5; :: thesis: A c= O
n in succ n by ORDINAL1:10;
then f . n in f .: (succ n) by A30, FUNCT_1:def 12;
then meet (f .: (succ n)) c= A1 by A31, SETFAM_1:4;
then S . n c= A1 by A6, A30;
hence A c= O by A29, XBOOLE_1:1; :: thesis: verum

end;

then reconsider B = B as Basis of x by A13, A19, A27, YELLOW_8:def 2;
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
thus for n, m being Element of NAT st m >= n holds
S . m c= S . n by A7; :: thesis: verum