let T be non empty T_0 TopSpace; :: thesis: ( T is finite implies weight T = card the carrier of T )
deffunc H₁( object ) -> set = meet { A where A is Element of the topology of T : $1 in A } ;
A1: for x being object st x in the carrier of T holds
H₁(x) in the carrier of (BoolePoset the carrier of T)

proof

let x be object ; :: thesis: ( x in the carrier of T implies H₁(x) in the carrier of (BoolePoset the carrier of T) )
assume A2: x in the carrier of T ; :: thesis: H₁(x) in the carrier of (BoolePoset the carrier of T)
the carrier of T in the topology of T by PRE_TOPC:def 1;
then the carrier of T in { A where A is Element of the topology of T : x in A } by A2;
then meet { A where A is Element of the topology of T : x in A } c= the carrier of T by SETFAM_1:3;
then meet { A where A is Element of the topology of T : x in A } in bool the carrier of T ;
hence H₁(x) in the carrier of (BoolePoset the carrier of T) by WAYBEL_7:2; :: thesis: verum

end;

consider f being Function of the carrier of T, the carrier of (BoolePoset the carrier of T) such that
A3: for x being object st x in the carrier of T holds
f . x = H₁(x) from FUNCT_2:sch 2(A1);
reconsider rf = rng f as Subset-Family of T by WAYBEL_7:2;
A4: 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 rf & p in a & a c= A )

proof

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 rf & p in a & a c= A ) )
assume A is open ; :: thesis: for p being Point of T st p in A holds
ex a being Subset of T st
( a in rf & p in a & a c= A )
then A5: A in the topology of T by PRE_TOPC:def 2;
let p be Point of T; :: thesis: ( p in A implies ex a being Subset of T st
( a in rf & p in a & a c= A ) )
assume p in A ; :: thesis: ex a being Subset of T st
( a in rf & p in a & a c= A )
then A6: A in { C where C is Element of the topology of T : p in C } by A5;
meet { C where C is Element of the topology of T : p in C } c= the carrier of T

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in meet { C where C is Element of the topology of T : p in C } or z in the carrier of T )
assume z in meet { C where C is Element of the topology of T : p in C } ; :: thesis: z in the carrier of T
then z in A by A6, SETFAM_1:def 1;
hence z in the carrier of T ; :: thesis: verum

end;

then reconsider a = meet { C where C is Element of the topology of T : p in C } as Subset of T ;
take a ; :: thesis: ( a in rf & p in a & a c= A )
p in the carrier of T ;
then A7: p in dom f by FUNCT_2:def 1;
a = f . p by A3;
hence a in rf by A7, FUNCT_1:def 3; :: thesis: ( p in a & a c= A )

now :: thesis: for Y being set st Y in { C where C is Element of the topology of T : p in C } holds
p in Y

let Y be set ; :: thesis: ( Y in { C where C is Element of the topology of T : p in C } implies p in Y )
assume Y in { C where C is Element of the topology of T : p in C } ; :: thesis: p in Y
then ex C being Element of the topology of T st
( Y = C & p in C ) ;
hence p in Y ; :: thesis: verum

end;

hence p in a by A6, SETFAM_1:def 1; :: thesis: a c= A
thus a c= A by A6, SETFAM_1:def 1; :: thesis: verum

end;

assume A8: T is finite ; :: thesis: weight T = card the carrier of T
rf c= the topology of T

proof

reconsider tT = the topology of T as non empty finite set by A8;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rf or z in the topology of T )
deffunc H₂( set ) -> set = $1;
assume z in rf ; :: thesis: z in the topology of T
then consider y being object such that
A9: ( y in dom f & z = f . y ) by FUNCT_1:def 3;
{ A where A is Element of the topology of T : y in A } c= bool the carrier of T

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { A where A is Element of the topology of T : y in A } or z in bool the carrier of T )
assume z in { A where A is Element of the topology of T : y in A } ; :: thesis: z in bool the carrier of T
then ex A being Element of the topology of T st
( z = A & y in A ) ;
hence z in bool the carrier of T ; :: thesis: verum

end;

then reconsider sfA = { A where A is Element of the topology of T : y in A } as Subset-Family of T ;
defpred S₁[ set ] means y in $1;
reconsider sfA = sfA as Subset-Family of T ;

now :: thesis: for P being Subset of T st P in sfA holds
P is open

let P be Subset of T; :: thesis: ( P in sfA implies P is open )
assume P in sfA ; :: thesis: P is open
then ex A being Element of the topology of T st
( P = A & y in A ) ;
hence P is open by PRE_TOPC:def 2; :: thesis: verum

end;

then A10: sfA is open by TOPS_2:def 1;
{ H₂(A) where A is Element of tT : S₁[A] } is finite from PRE_CIRC:sch 1();
then A11: meet sfA is open by A10, TOPS_2:20;
z = meet { A where A is Element of the topology of T : y in A } by A3, A9;
hence z in the topology of T by A11, PRE_TOPC:def 2; :: thesis: verum

end;

then rng f is Basis of T by A4, YELLOW_9:32;
then A12: card (rng f) in { (card B1) where B1 is Basis of T : verum } ;
then A13: meet { (card B1) where B1 is Basis of T : verum } c= card (rng f) by SETFAM_1:3;

now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
not x1 <> x2

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies not x1 <> x2 )
assume that
A14: ( x1 in dom f & x2 in dom f ) and
A15: f . x1 = f . x2 ; :: thesis: not x1 <> x2
reconsider x3 = x1, x4 = x2 as Point of T by A14;
assume x1 <> x2 ; :: thesis: contradiction
then consider V being Subset of T such that
A16: V is open and
A17: ( ( x3 in V & not x4 in V ) or ( x4 in V & not x3 in V ) ) by T_0TOPSP:def 7;
A18: ( f . x3 = meet { A where A is Element of the topology of T : x3 in A } & f . x4 = meet { A where A is Element of the topology of T : x4 in A } ) by A3;

now :: thesis: contradiction

per cases ( ( x3 in V & not x4 in V ) or ( x4 in V & not x3 in V ) ) by A17;

suppose A19: ( x3 in V & not x4 in V ) ; :: thesis: contradiction

V in the topology of T by A16, PRE_TOPC:def 2;
then A20: V in { A where A is Element of the topology of T : x3 in A } by A19;
A21: meet { A where A is Element of the topology of T : x3 in A } c= V by A20, SETFAM_1:def 1;

A22: now :: thesis: for Y being set st Y in { A where A is Element of the topology of T : x4 in A } holds
x4 in Y

let Y be set ; :: thesis: ( Y in { A where A is Element of the topology of T : x4 in A } implies x4 in Y )
assume Y in { A where A is Element of the topology of T : x4 in A } ; :: thesis: x4 in Y
then ex A being Element of the topology of T st
( Y = A & x4 in A ) ;
hence x4 in Y ; :: thesis: verum

end;

the carrier of T in the topology of T by PRE_TOPC:def 1;
then the carrier of T in { A where A is Element of the topology of T : x4 in A } ;
then x4 in meet { A where A is Element of the topology of T : x3 in A } by A15, A18, A22, SETFAM_1:def 1;
hence contradiction by A19, A21; :: thesis: verum

end;

suppose A23: ( x4 in V & not x3 in V ) ; :: thesis: contradiction

V in the topology of T by A16, PRE_TOPC:def 2;
then A24: V in { A where A is Element of the topology of T : x4 in A } by A23;
A25: meet { A where A is Element of the topology of T : x4 in A } c= V by A24, SETFAM_1:def 1;

A26: now :: thesis: for Y being set st Y in { A where A is Element of the topology of T : x3 in A } holds
x3 in Y

let Y be set ; :: thesis: ( Y in { A where A is Element of the topology of T : x3 in A } implies x3 in Y )
assume Y in { A where A is Element of the topology of T : x3 in A } ; :: thesis: x3 in Y
then ex A being Element of the topology of T st
( Y = A & x3 in A ) ;
hence x3 in Y ; :: thesis: verum

end;

the carrier of T in the topology of T by PRE_TOPC:def 1;
then the carrier of T in { A where A is Element of the topology of T : x3 in A } ;
then x3 in meet { A where A is Element of the topology of T : x4 in A } by A15, A18, A26, SETFAM_1:def 1;
hence contradiction by A23, A25; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

then ( dom f = the carrier of T & f is one-to-one ) by FUNCT_1:def 4, FUNCT_2:def 1;
then A27: the carrier of T, rng f are_equipotent by WELLORD2:def 4;
for X being set st X in { (card B1) where B1 is Basis of T : verum } holds
card (rng f) c= X

proof

let X be set ; :: thesis: ( X in { (card B1) where B1 is Basis of T : verum } implies card (rng f) c= X )
assume X in { (card B1) where B1 is Basis of T : verum } ; :: thesis: card (rng f) c= X
then consider B2 being Basis of T such that
A28: X = card B2 ;
rng f c= B2

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in B2 )
assume y in rng f ; :: thesis: y in B2
then consider x being object such that
A29: x in dom f and
A30: y = f . x by FUNCT_1:def 3;
reconsider x1 = x as Element of T by A29;
y = meet { A where A is Element of the topology of T : x1 in A } by A3, A30;
hence y in B2 by A8, YELLOW15:31; :: thesis: verum

end;

hence card (rng f) c= X by A28, CARD_1:11; :: thesis: verum

end;

then card (rng f) c= meet { (card B1) where B1 is Basis of T : verum } by A12, SETFAM_1:5;
then card (rng f) = meet { (card B1) where B1 is Basis of T : verum } by A13, XBOOLE_0:def 10
.= weight T by WAYBEL23:def 5 ;
hence weight T = card the carrier of T by A27, CARD_1:5; :: thesis: verum