let T be infinite-weight TopSpace; :: thesis: for B being Basis of T ex B1 being Basis of T st
( B1 c= B & card B1 = weight T )
let B be Basis of T; :: thesis: ex B1 being Basis of T st
( B1 c= B & card B1 = weight T )
consider B0 being Basis of T such that
A1:
card B0 = weight T
by WAYBEL23:75;
A2:
not weight T is finite
by Def4;
defpred S1[ set , set ] means ( union $2 = $1 & card $2 c= weight T );
A3:
now let a be
set ;
:: thesis: ( a in B0 implies ex b being set st
( b in bool B & S1[a,b] ) )assume
a in B0
;
:: thesis: ex b being set st
( b in bool B & S1[a,b] )then reconsider W =
a as
open Subset of
T by YELLOW_8:19;
set Sa =
{ U where U is Subset of T : ( U in B & U c= a ) } ;
A4:
{ U where U is Subset of T : ( U in B & U c= a ) } c= B
A5:
union { U where U is Subset of T : ( U in B & U c= a ) } = W
by YELLOW_8:18;
(
B is
open &
{ U where U is Subset of T : ( U in B & U c= a ) } c= bool the
carrier of
T )
by A4, XBOOLE_1:1, YELLOW_9:27;
then reconsider Sa =
{ U where U is Subset of T : ( U in B & U c= a ) } as
open Subset-Family of
T by A4, TOPS_2:18;
consider G being
open Subset-Family of
T such that A6:
(
G c= Sa &
union G = union Sa &
card G c= weight T )
by Th12;
reconsider b =
G as
set ;
take b =
b;
:: thesis: ( b in bool B & S1[a,b] )
b c= B
by A4, A6, XBOOLE_1:1;
hence
b in bool B
;
:: thesis: S1[a,b]thus
S1[
a,
b]
by A5, A6;
:: thesis: verum end;
consider f being Function such that
A7:
( dom f = B0 & rng f c= bool B )
and
A8:
for a being set st a in B0 holds
S1[a,f . a]
from WELLORD2:sch 1(A3);
A10:
Union f c= union (bool B)
by A7, ZFMISC_1:95;
then A11:
Union f c= B
by ZFMISC_1:99;
then reconsider B1 = Union f as Subset-Family of T by XBOOLE_1:1;
now
B c= the
topology of
T
by CANTOR_1:def 2;
hence
B1 c= the
topology of
T
by A11, XBOOLE_1:1;
:: thesis: for A being Subset of T st A is open holds
for p being Point of T st p in A holds
ex a being Subset of T st
( a in B1 & p in a & a c= A )let A be
Subset of
T;
:: thesis: ( A is open implies for p being Point of T st p in A holds
ex a being Subset of T st
( a in B1 & p in a & a c= A ) )assume A12:
A is
open
;
:: thesis: for p being Point of T st p in A holds
ex a being Subset of T st
( a in B1 & p in a & a c= A )let p be
Point of
T;
:: thesis: ( p in A implies ex a being Subset of T st
( a in B1 & p in a & a c= A ) )assume
p in A
;
:: thesis: ex a being Subset of T st
( a in B1 & p in a & a c= A )then consider U being
Subset of
T such that A13:
(
U in B0 &
p in U &
U c= A )
by A12, YELLOW_9:31;
A14:
S1[
U,
f . U]
by A8, A13;
then consider a being
set such that A15:
(
p in a &
a in f . U )
by A13, TARSKI:def 4;
A16:
a in B1
by A7, A13, A15, CARD_5:10;
a c= U
by A14, A15, ZFMISC_1:92;
hence
ex
a being
Subset of
T st
(
a in B1 &
p in a &
a c= A )
by A13, A15, A16, XBOOLE_1:1;
:: thesis: verum end;
then reconsider B1 = B1 as Basis of T by YELLOW_9:32;
take
B1
; :: thesis: ( B1 c= B & card B1 = weight T )
thus
B1 c= B
by A10, ZFMISC_1:99; :: thesis: card B1 = weight T
then
card B1 c= (weight T) *` (weight T)
by CARD_3:133;
hence
card B1 c= weight T
by A2, CARD_4:77; :: according to XBOOLE_0:def 10 :: thesis: weight T c= card B1
thus
weight T c= card B1
by WAYBEL23:74; :: thesis: verum