let T be non empty TopSpace; :: thesis: ( T is metrizable implies ex Un being FamilySequence of T st Un is Basis_sigma_discrete )

assume A1: T is metrizable ; :: thesis: ex Un being FamilySequence of T st Un is Basis_sigma_discrete

consider metr being Function of [: the carrier of T, the carrier of T:],REAL such that

A2: metr is_metric_of the carrier of T and

A3: Family_open_set (SpaceMetr ( the carrier of T,metr)) = the topology of T by A1, PCOMPS_1:def 8;

set bbcT = bool (bool the carrier of T);

reconsider PM = SpaceMetr ( the carrier of T,metr) as non empty MetrSpace by A2, PCOMPS_1:36;

deffunc H_{1}( object ) -> set = { (Ball (x,(1 / (2 |^ (In ($1,NAT)))))) where x is Point of PM : x is Point of PM } ;

A4: for k being object st k in NAT holds

H_{1}(k) in bool (bool the carrier of T)

A5: for k being object st k in NAT holds

FB . k = H_{1}(k)
from FUNCT_2:sch 2(A4);

defpred S_{1}[ set , set ] means ex FS being FamilySequence of T st

( $2 = FS & Union FS is open & Union FS is Cover of T & Union FS is_finer_than FB . $1 & FS is sigma_discrete );

set TPM = TopSpaceMetr PM;

A6: TopSpaceMetr PM = TopStruct(# the carrier of PM,(Family_open_set PM) #) by PCOMPS_1:def 5;

then A7: [#] T = [#] (TopSpaceMetr PM) by A2, PCOMPS_2:4;

A8: for n being Element of NAT ex Un being Element of Funcs (NAT,(bool (bool the carrier of T))) st S_{1}[n,Un]

A17: for n being Element of NAT holds S_{1}[n,Un . n]
from FUNCT_2:sch 3(A8);

defpred S_{2}[ object , object ] means for n, m being Nat st PairFunc . [n,m] = $1 holds

for Unn being FamilySequence of T st Unn = Un . n holds

$2 = Unn . m;

A18: for k being object st k in NAT holds

ex Ux being object st

( Ux in bool (bool the carrier of T) & S_{2}[k,Ux] )

A27: for k being object st k in NAT holds

S_{2}[k,UX . k]
from FUNCT_2:sch 1(A18);

A28: for A being Subset of T st A is open holds

for p being Point of T st p in A holds

ex B being Subset of T st

( B in Union UX & p in B & B c= A )

Union UX c= the topology of T

then UX is Basis_sigma_discrete by A53, NAGATA_1:def 5;

hence ex Un being FamilySequence of T st Un is Basis_sigma_discrete ; :: thesis: verum

assume A1: T is metrizable ; :: thesis: ex Un being FamilySequence of T st Un is Basis_sigma_discrete

consider metr being Function of [: the carrier of T, the carrier of T:],REAL such that

A2: metr is_metric_of the carrier of T and

A3: Family_open_set (SpaceMetr ( the carrier of T,metr)) = the topology of T by A1, PCOMPS_1:def 8;

set bbcT = bool (bool the carrier of T);

reconsider PM = SpaceMetr ( the carrier of T,metr) as non empty MetrSpace by A2, PCOMPS_1:36;

deffunc H

A4: for k being object st k in NAT holds

H

proof

consider FB being FamilySequence of T such that
let k be object ; :: thesis: ( k in NAT implies H_{1}(k) in bool (bool the carrier of T) )

assume k in NAT ; :: thesis: H_{1}(k) in bool (bool the carrier of T)

then reconsider k = k as Element of NAT ;

H_{1}(k) c= bool the carrier of T
_{1}(k) in bool (bool the carrier of T)
; :: thesis: verum

end;assume k in NAT ; :: thesis: H

then reconsider k = k as Element of NAT ;

H

proof

hence
H
let B be object ; :: according to TARSKI:def 3 :: thesis: ( not B in H_{1}(k) or B in bool the carrier of T )

assume B in H_{1}(k)
; :: thesis: B in bool the carrier of T

then ex x being Point of PM st

( B = Ball (x,(1 / (2 |^ k))) & x is Point of PM ) ;

then B in Family_open_set PM by PCOMPS_1:29;

hence B in bool the carrier of T by A3; :: thesis: verum

end;assume B in H

then ex x being Point of PM st

( B = Ball (x,(1 / (2 |^ k))) & x is Point of PM ) ;

then B in Family_open_set PM by PCOMPS_1:29;

hence B in bool the carrier of T by A3; :: thesis: verum

A5: for k being object st k in NAT holds

FB . k = H

defpred S

( $2 = FS & Union FS is open & Union FS is Cover of T & Union FS is_finer_than FB . $1 & FS is sigma_discrete );

set TPM = TopSpaceMetr PM;

A6: TopSpaceMetr PM = TopStruct(# the carrier of PM,(Family_open_set PM) #) by PCOMPS_1:def 5;

then A7: [#] T = [#] (TopSpaceMetr PM) by A2, PCOMPS_2:4;

A8: for n being Element of NAT ex Un being Element of Funcs (NAT,(bool (bool the carrier of T))) st S

proof

consider Un being sequence of (Funcs (NAT,(bool (bool the carrier of T)))) such that
let n be Element of NAT ; :: thesis: ex Un being Element of Funcs (NAT,(bool (bool the carrier of T))) st S_{1}[n,Un]

A10: [#] (TopSpaceMetr PM) c= union (FB . n)

then FB . n is Cover of T by A7, SETFAM_1:45;

then consider Un being FamilySequence of T such that

A16: ( Union Un is open & Union Un is Cover of T & Union Un is_finer_than FB . n & Un is sigma_discrete ) by A1, A9, Th20;

Un in Funcs (NAT,(bool (bool the carrier of T))) by FUNCT_2:8;

hence ex Un being Element of Funcs (NAT,(bool (bool the carrier of T))) st S_{1}[n,Un]
by A16; :: thesis: verum

end;now :: thesis: for U being Subset of T st U in FB . n holds

U is open

then A9:
FB . n is open
;U is open

let U be Subset of T; :: thesis: ( U in FB . n implies U is open )

assume U in FB . n ; :: thesis: U is open

then U in H_{1}(n)
by A5;

then ex x being Point of PM st

( U = Ball (x,(1 / (2 |^ n))) & x is Point of PM ) ;

then U in the topology of T by A3, PCOMPS_1:29;

hence U is open by PRE_TOPC:def 2; :: thesis: verum

end;assume U in FB . n ; :: thesis: U is open

then U in H

then ex x being Point of PM st

( U = Ball (x,(1 / (2 |^ n))) & x is Point of PM ) ;

then U in the topology of T by A3, PCOMPS_1:29;

hence U is open by PRE_TOPC:def 2; :: thesis: verum

A10: [#] (TopSpaceMetr PM) c= union (FB . n)

proof

union (FB . n) c= [#] (TopSpaceMetr PM)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] (TopSpaceMetr PM) or x in union (FB . n) )

assume x in [#] (TopSpaceMetr PM) ; :: thesis: x in union (FB . n)

then reconsider x9 = x as Element of PM by A6;

2 |^ n > 0 by NEWTON:83;

then A11: x9 in Ball (x9,(1 / (2 |^ n))) by TBSP_1:11, XREAL_1:139;

Ball (x9,(1 / (2 |^ n))) in H_{1}(n)
;

then Ball (x9,(1 / (2 |^ n))) in FB . n by A5;

hence x in union (FB . n) by A11, TARSKI:def 4; :: thesis: verum

end;assume x in [#] (TopSpaceMetr PM) ; :: thesis: x in union (FB . n)

then reconsider x9 = x as Element of PM by A6;

2 |^ n > 0 by NEWTON:83;

then A11: x9 in Ball (x9,(1 / (2 |^ n))) by TBSP_1:11, XREAL_1:139;

Ball (x9,(1 / (2 |^ n))) in H

then Ball (x9,(1 / (2 |^ n))) in FB . n by A5;

hence x in union (FB . n) by A11, TARSKI:def 4; :: thesis: verum

proof

then
[#] (TopSpaceMetr PM) = union (FB . n)
by A10;
given x being object such that A12:
x in union (FB . n)
and

A13: not x in [#] (TopSpaceMetr PM) ; :: according to TARSKI:def 3 :: thesis: contradiction

consider A being set such that

A14: x in A and

A15: A in FB . n by A12, TARSKI:def 4;

A in H_{1}(n)
by A5, A15;

then ex y being Point of PM st

( A = Ball (y,(1 / (2 |^ n))) & y is Point of PM ) ;

hence contradiction by A6, A13, A14; :: thesis: verum

end;A13: not x in [#] (TopSpaceMetr PM) ; :: according to TARSKI:def 3 :: thesis: contradiction

consider A being set such that

A14: x in A and

A15: A in FB . n by A12, TARSKI:def 4;

A in H

then ex y being Point of PM st

( A = Ball (y,(1 / (2 |^ n))) & y is Point of PM ) ;

hence contradiction by A6, A13, A14; :: thesis: verum

then FB . n is Cover of T by A7, SETFAM_1:45;

then consider Un being FamilySequence of T such that

A16: ( Union Un is open & Union Un is Cover of T & Union Un is_finer_than FB . n & Un is sigma_discrete ) by A1, A9, Th20;

Un in Funcs (NAT,(bool (bool the carrier of T))) by FUNCT_2:8;

hence ex Un being Element of Funcs (NAT,(bool (bool the carrier of T))) st S

A17: for n being Element of NAT holds S

defpred S

for Unn being FamilySequence of T st Unn = Un . n holds

$2 = Unn . m;

A18: for k being object st k in NAT holds

ex Ux being object st

( Ux in bool (bool the carrier of T) & S

proof

consider UX being sequence of (bool (bool the carrier of T)) such that
let k be object ; :: thesis: ( k in NAT implies ex Ux being object st

( Ux in bool (bool the carrier of T) & S_{2}[k,Ux] ) )

assume k in NAT ; :: thesis: ex Ux being object st

( Ux in bool (bool the carrier of T) & S_{2}[k,Ux] )

then reconsider k9 = k as Element of NAT ;

NAT = rng PairFunc by Th2, FUNCT_2:def 3;

then consider nm being object such that

A19: nm in dom PairFunc and

A20: k9 = PairFunc . nm by FUNCT_1:def 3;

consider n, m being object such that

A21: n in NAT and

A22: m in NAT and

A23: nm = [n,m] by A19, ZFMISC_1:def 2;

reconsider Unn = Un . n as FamilySequence of T by A21, FUNCT_2:5, FUNCT_2:66;

take Ux = Unn . m; :: thesis: ( Ux in bool (bool the carrier of T) & S_{2}[k,Ux] )

dom Unn = NAT by PARTFUN1:def 2;

then m in dom Unn by A22;

then Ux in rng Unn by FUNCT_1:3;

hence Ux in bool (bool the carrier of T) ; :: thesis: S_{2}[k,Ux]

let n1, m1 be Nat; :: thesis: ( PairFunc . [n1,m1] = k implies for Unn being FamilySequence of T st Unn = Un . n1 holds

Ux = Unn . m1 )

assume A24: PairFunc . [n1,m1] = k ; :: thesis: for Unn being FamilySequence of T st Unn = Un . n1 holds

Ux = Unn . m1

reconsider nn1 = n1, mm1 = m1 as Element of NAT by ORDINAL1:def 12;

Ux = Unn . m1 ; :: thesis: verum

end;( Ux in bool (bool the carrier of T) & S

assume k in NAT ; :: thesis: ex Ux being object st

( Ux in bool (bool the carrier of T) & S

then reconsider k9 = k as Element of NAT ;

NAT = rng PairFunc by Th2, FUNCT_2:def 3;

then consider nm being object such that

A19: nm in dom PairFunc and

A20: k9 = PairFunc . nm by FUNCT_1:def 3;

consider n, m being object such that

A21: n in NAT and

A22: m in NAT and

A23: nm = [n,m] by A19, ZFMISC_1:def 2;

reconsider Unn = Un . n as FamilySequence of T by A21, FUNCT_2:5, FUNCT_2:66;

take Ux = Unn . m; :: thesis: ( Ux in bool (bool the carrier of T) & S

dom Unn = NAT by PARTFUN1:def 2;

then m in dom Unn by A22;

then Ux in rng Unn by FUNCT_1:3;

hence Ux in bool (bool the carrier of T) ; :: thesis: S

let n1, m1 be Nat; :: thesis: ( PairFunc . [n1,m1] = k implies for Unn being FamilySequence of T st Unn = Un . n1 holds

Ux = Unn . m1 )

assume A24: PairFunc . [n1,m1] = k ; :: thesis: for Unn being FamilySequence of T st Unn = Un . n1 holds

Ux = Unn . m1

reconsider nn1 = n1, mm1 = m1 as Element of NAT by ORDINAL1:def 12;

now :: thesis: for Unn being FamilySequence of T st Unn = Un . nn1 holds

Ux = Unn . mm1

hence
for Unn being FamilySequence of T st Unn = Un . n1 holds Ux = Unn . mm1

let Unn be FamilySequence of T; :: thesis: ( Unn = Un . nn1 implies Ux = Unn . mm1 )

assume A25: Unn = Un . nn1 ; :: thesis: Ux = Unn . mm1

A26: [n,m] = [nn1,mm1] by A19, A20, A23, A24, Th2, FUNCT_2:19;

then n1 = n by XTUPLE_0:1;

hence Ux = Unn . mm1 by A25, A26, XTUPLE_0:1; :: thesis: verum

end;assume A25: Unn = Un . nn1 ; :: thesis: Ux = Unn . mm1

A26: [n,m] = [nn1,mm1] by A19, A20, A23, A24, Th2, FUNCT_2:19;

then n1 = n by XTUPLE_0:1;

hence Ux = Unn . mm1 by A25, A26, XTUPLE_0:1; :: thesis: verum

Ux = Unn . m1 ; :: thesis: verum

A27: for k being object st k in NAT holds

S

A28: for A being Subset of T st A is open holds

for p being Point of T st p in A holds

ex B being Subset of T st

( B in Union UX & p in B & B c= A )

proof

for k being Element of NAT holds UX . k is discrete
let A be Subset of T; :: thesis: ( A is open implies for p being Point of T st p in A holds

ex B being Subset of T st

( B in Union UX & p in B & B c= A ) )

assume A is open ; :: thesis: for p being Point of T st p in A holds

ex B being Subset of T st

( B in Union UX & p in B & B c= A )

then A29: A in Family_open_set PM by A3, PRE_TOPC:def 2;

let p be Point of T; :: thesis: ( p in A implies ex B being Subset of T st

( B in Union UX & p in B & B c= A ) )

assume A30: p in A ; :: thesis: ex B being Subset of T st

( B in Union UX & p in B & B c= A )

reconsider p = p as Element of PM by A30, A29;

consider r being Real such that

A31: r > 0 and

A32: Ball (p,r) c= A by A30, A29, PCOMPS_1:def 4;

consider n being Nat such that

A33: 1 / (2 |^ n) <= r by A31, PREPOWER:92;

consider Unn1 being FamilySequence of T such that

A34: Un . (n + 1) = Unn1 and

Union Unn1 is open and

A35: Union Unn1 is Cover of T and

A36: Union Unn1 is_finer_than FB . (n + 1) and

Unn1 is sigma_discrete by A17;

union (Union Unn1) = [#] T by A35, SETFAM_1:45;

then consider B being set such that

A37: p in B and

A38: B in Union Unn1 by TARSKI:def 4;

reconsider B = B as Subset of PM by A2, A38, PCOMPS_2:4;

consider B1 being set such that

A39: B1 in FB . (n + 1) and

A40: B c= B1 by A36, A38, SETFAM_1:def 2;

consider k being Nat such that

A41: B in Unn1 . k by A38, PROB_1:12;

( n + 1 = In ((n + 1),NAT) & B1 in H_{1}(n + 1) )
by A5, A39;

then consider q being Point of PM such that

A42: B1 = Ball (q,(1 / (2 |^ (n + 1)))) and

q is Element of PM ;

reconsider kk = k as Element of NAT by ORDINAL1:def 12;

UX . (PairFunc . [(n + 1),kk]) = Unn1 . kk by A27, A34;

then B in Union UX by A41, PROB_1:12;

hence ex B being Subset of T st

( B in Union UX & p in B & B c= A ) by A32, A37, A44, XBOOLE_1:1; :: thesis: verum

end;ex B being Subset of T st

( B in Union UX & p in B & B c= A ) )

assume A is open ; :: thesis: for p being Point of T st p in A holds

ex B being Subset of T st

( B in Union UX & p in B & B c= A )

then A29: A in Family_open_set PM by A3, PRE_TOPC:def 2;

let p be Point of T; :: thesis: ( p in A implies ex B being Subset of T st

( B in Union UX & p in B & B c= A ) )

assume A30: p in A ; :: thesis: ex B being Subset of T st

( B in Union UX & p in B & B c= A )

reconsider p = p as Element of PM by A30, A29;

consider r being Real such that

A31: r > 0 and

A32: Ball (p,r) c= A by A30, A29, PCOMPS_1:def 4;

consider n being Nat such that

A33: 1 / (2 |^ n) <= r by A31, PREPOWER:92;

consider Unn1 being FamilySequence of T such that

A34: Un . (n + 1) = Unn1 and

Union Unn1 is open and

A35: Union Unn1 is Cover of T and

A36: Union Unn1 is_finer_than FB . (n + 1) and

Unn1 is sigma_discrete by A17;

union (Union Unn1) = [#] T by A35, SETFAM_1:45;

then consider B being set such that

A37: p in B and

A38: B in Union Unn1 by TARSKI:def 4;

reconsider B = B as Subset of PM by A2, A38, PCOMPS_2:4;

consider B1 being set such that

A39: B1 in FB . (n + 1) and

A40: B c= B1 by A36, A38, SETFAM_1:def 2;

consider k being Nat such that

A41: B in Unn1 . k by A38, PROB_1:12;

( n + 1 = In ((n + 1),NAT) & B1 in H

then consider q being Point of PM such that

A42: B1 = Ball (q,(1 / (2 |^ (n + 1)))) and

q is Element of PM ;

now :: thesis: for s being Element of PM st s in B holds

s in Ball (p,r)

then A44:
B c= Ball (p,r)
;s in Ball (p,r)

let s be Element of PM; :: thesis: ( s in B implies s in Ball (p,r) )

assume s in B ; :: thesis: s in Ball (p,r)

then A43: dist (q,s) < 1 / (2 |^ (n + 1)) by A40, A42, METRIC_1:11;

dist (q,p) < 1 / (2 |^ (n + 1)) by A37, A40, A42, METRIC_1:11;

then ( dist (p,s) <= (dist (q,p)) + (dist (q,s)) & (dist (q,p)) + (dist (q,s)) < (1 / (2 |^ (n + 1))) + (1 / (2 |^ (n + 1))) ) by A43, METRIC_1:4, XREAL_1:8;

then dist (p,s) < 2 * (1 / (2 |^ (n + 1))) by XXREAL_0:2;

then dist (p,s) < (1 / ((2 |^ n) * 2)) * 2 by NEWTON:6;

then dist (p,s) < 1 / (2 |^ n) by XCMPLX_1:92;

then dist (p,s) < r by A33, XXREAL_0:2;

hence s in Ball (p,r) by METRIC_1:11; :: thesis: verum

end;assume s in B ; :: thesis: s in Ball (p,r)

then A43: dist (q,s) < 1 / (2 |^ (n + 1)) by A40, A42, METRIC_1:11;

dist (q,p) < 1 / (2 |^ (n + 1)) by A37, A40, A42, METRIC_1:11;

then ( dist (p,s) <= (dist (q,p)) + (dist (q,s)) & (dist (q,p)) + (dist (q,s)) < (1 / (2 |^ (n + 1))) + (1 / (2 |^ (n + 1))) ) by A43, METRIC_1:4, XREAL_1:8;

then dist (p,s) < 2 * (1 / (2 |^ (n + 1))) by XXREAL_0:2;

then dist (p,s) < (1 / ((2 |^ n) * 2)) * 2 by NEWTON:6;

then dist (p,s) < 1 / (2 |^ n) by XCMPLX_1:92;

then dist (p,s) < r by A33, XXREAL_0:2;

hence s in Ball (p,r) by METRIC_1:11; :: thesis: verum

reconsider kk = k as Element of NAT by ORDINAL1:def 12;

UX . (PairFunc . [(n + 1),kk]) = Unn1 . kk by A27, A34;

then B in Union UX by A41, PROB_1:12;

hence ex B being Subset of T st

( B in Union UX & p in B & B c= A ) by A32, A37, A44, XBOOLE_1:1; :: thesis: verum

proof

then A53:
UX is sigma_discrete
by NAGATA_1:def 2;
let k be Nat; :: thesis: ( k is Element of NAT implies UX . k is discrete )

A45: k in NAT by ORDINAL1:def 12;

NAT = rng PairFunc by Th2, FUNCT_2:def 3;

then consider nm being object such that

A46: nm in dom PairFunc and

A47: k = PairFunc . nm by FUNCT_1:def 3, A45;

consider n, m being object such that

A48: n in NAT and

A49: m in NAT and

A50: nm = [n,m] by A46, ZFMISC_1:def 2;

consider FS being FamilySequence of T such that

A51: Un . n = FS and

Union FS is open and

Union FS is Cover of T and

Union FS is_finer_than FB . n and

A52: FS is sigma_discrete by A17, A48;

dom FS = NAT by PARTFUN1:def 2;

then m in dom FS by A49;

then FS . m in rng FS by FUNCT_1:3;

then FS . m in bool (bool the carrier of T) ;

then reconsider FSm = FS . m as Subset-Family of T ;

FSm is discrete by A49, A52, NAGATA_1:def 2;

hence ( k is Element of NAT implies UX . k is discrete ) by A27, A47, A48, A49, A50, A51; :: thesis: verum

end;A45: k in NAT by ORDINAL1:def 12;

NAT = rng PairFunc by Th2, FUNCT_2:def 3;

then consider nm being object such that

A46: nm in dom PairFunc and

A47: k = PairFunc . nm by FUNCT_1:def 3, A45;

consider n, m being object such that

A48: n in NAT and

A49: m in NAT and

A50: nm = [n,m] by A46, ZFMISC_1:def 2;

consider FS being FamilySequence of T such that

A51: Un . n = FS and

Union FS is open and

Union FS is Cover of T and

Union FS is_finer_than FB . n and

A52: FS is sigma_discrete by A17, A48;

dom FS = NAT by PARTFUN1:def 2;

then m in dom FS by A49;

then FS . m in rng FS by FUNCT_1:3;

then FS . m in bool (bool the carrier of T) ;

then reconsider FSm = FS . m as Subset-Family of T ;

FSm is discrete by A49, A52, NAGATA_1:def 2;

hence ( k is Element of NAT implies UX . k is discrete ) by A27, A47, A48, A49, A50, A51; :: thesis: verum

Union UX c= the topology of T

proof

then
Union UX is Basis of T
by A28, YELLOW_9:32;
let UXk be object ; :: according to TARSKI:def 3 :: thesis: ( not UXk in Union UX or UXk in the topology of T )

assume UXk in Union UX ; :: thesis: UXk in the topology of T

then consider k being Nat such that

A54: UXk in UX . k by PROB_1:12;

reconsider UXk9 = UXk as Subset of T by A54;

A55: k in NAT by ORDINAL1:def 12;

NAT = rng PairFunc by Th2, FUNCT_2:def 3;

then consider nm being object such that

A56: nm in dom PairFunc and

A57: k = PairFunc . nm by FUNCT_1:def 3, A55;

consider n, m being object such that

A58: n in NAT and

A59: m in NAT and

A60: nm = [n,m] by A56, ZFMISC_1:def 2;

reconsider Unn = Un . n as FamilySequence of T by A58, FUNCT_2:5, FUNCT_2:66;

UXk in Unn . m by A27, A54, A57, A58, A59, A60, A55;

then A61: UXk in Union Unn by A59, PROB_1:12;

ex FS being FamilySequence of T st

( Un . n = FS & Union FS is open & Union FS is Cover of T & Union FS is_finer_than FB . n & FS is sigma_discrete ) by A17, A58;

then UXk9 is open by A61;

hence UXk in the topology of T by PRE_TOPC:def 2; :: thesis: verum

end;assume UXk in Union UX ; :: thesis: UXk in the topology of T

then consider k being Nat such that

A54: UXk in UX . k by PROB_1:12;

reconsider UXk9 = UXk as Subset of T by A54;

A55: k in NAT by ORDINAL1:def 12;

NAT = rng PairFunc by Th2, FUNCT_2:def 3;

then consider nm being object such that

A56: nm in dom PairFunc and

A57: k = PairFunc . nm by FUNCT_1:def 3, A55;

consider n, m being object such that

A58: n in NAT and

A59: m in NAT and

A60: nm = [n,m] by A56, ZFMISC_1:def 2;

reconsider Unn = Un . n as FamilySequence of T by A58, FUNCT_2:5, FUNCT_2:66;

UXk in Unn . m by A27, A54, A57, A58, A59, A60, A55;

then A61: UXk in Union Unn by A59, PROB_1:12;

ex FS being FamilySequence of T st

( Un . n = FS & Union FS is open & Union FS is Cover of T & Union FS is_finer_than FB . n & FS is sigma_discrete ) by A17, A58;

then UXk9 is open by A61;

hence UXk in the topology of T by PRE_TOPC:def 2; :: thesis: verum

then UX is Basis_sigma_discrete by A53, NAGATA_1:def 5;

hence ex Un being FamilySequence of T st Un is Basis_sigma_discrete ; :: thesis: verum