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

proof

let x be set ; :: thesis: ( x in the carrier of T implies H₁(x) in the carrier of (BoolePoset the carrier of T) )
A3: the carrier of T in the topology of T by PRE_TOPC:def 1;
assume x in the carrier of T ; :: thesis: H₁(x) in the carrier of (BoolePoset the carrier of T)
then the carrier of T in { A where A is Element of the topology of T : x in A } by A3;
then meet { A where A is Element of the topology of T : x in A } c= the carrier of T by SETFAM_1:4;
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:4; :: thesis: verum

end;

consider f being Function of the carrier of T,the carrier of (BoolePoset the carrier of T) such that
A4: for x being set st x in the carrier of T holds
f . x = H₁(x) from FUNCT_2:sch 2(A2);
reconsider rf = rng f as Subset-Family of T by WAYBEL_7:4;
A5: rf c= the topology of T

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rf or z in the topology of T )
assume z in rf ; :: thesis: z in the topology of T
then consider y being set such that
A6: y in dom f and
A7: z = f . y by FUNCT_1:def 5;
A8: z = meet { A where A is Element of the topology of T : y in A } by A4, A6, A7;
{ A where A is Element of the topology of T : y in A } c= bool the carrier of T

proof

let z be set ; :: 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 consider A being Element of the topology of T such that
A9: z = A and
y in A ;
thus z in bool the carrier of T by A9; :: thesis: verum

end;

then reconsider sfA = { A where A is Element of the topology of T : y in A } as Subset-Family of T ;
reconsider sfA = sfA as Subset-Family of T ;

now

let P be Subset of T; :: thesis: ( P in sfA implies P is open )
assume P in sfA ; :: thesis: P is open
then consider A being Element of the topology of T such that
A10: P = A and
y in A ;
thus P is open by A10, PRE_TOPC:def 5; :: thesis: verum

end;

then A11: sfA is open by TOPS_2:def 1;
the carrier of T is finite by A1;
then reconsider tT = the topology of T as non empty finite set ;
deffunc H₂( set ) -> set = $1;
defpred S₁[ set ] means y in $1;
{ H₂(A) where A is Element of tT : S₁[A] } is finite from PRE_CIRC:sch 1();
then meet sfA is open by A11, TOPS_2:27;
hence z in the topology of T by A8, PRE_TOPC:def 5; :: thesis: verum

end;

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 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 rf & 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 rf & p in a & a c= A ) )
assume A13: p in A ; :: thesis: ex a being Subset of T st
( a in rf & p in a & a c= A )
A in the topology of T by A12, PRE_TOPC:def 5;
then A14: A in { C where C is Element of the topology of T : p in C } by A13;
meet { C where C is Element of the topology of T : p in C } c= the carrier of T

proof

let z be set ; :: 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 A14, 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 A15: p in dom f by FUNCT_2:def 1;
a = f . p by A4;
hence a in rf by A15, FUNCT_1:def 5; :: thesis: ( p in a & a c= A )

now

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 consider C being Element of the topology of T such that
A16: Y = C and
A17: p in C ;
thus p in Y by A16, A17; :: thesis: verum

end;

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

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in a or z in A )
assume z in a ; :: thesis: z in A
hence z in A by A14, SETFAM_1:def 1; :: thesis: verum

end;

end;

then rng f is Basis of T by A5, YELLOW_9:32;
then A18: card (rng f) in { (card B1) where B1 is Basis of T : verum } ;
then A19: meet { (card B1) where B1 is Basis of T : verum } c= card (rng f) by SETFAM_1: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
A20: X = card B2 ;
rng f c= B2

proof

let y be set ; :: 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 set such that
A21: x in dom f and
A22: y = f . x by FUNCT_1:def 5;
reconsider x1 = x as Element of T by A21;
y = meet { A where A is Element of the topology of T : x1 in A } by A4, A22;
hence y in B2 by A1, YELLOW15:32; :: thesis: verum

end;

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

end;

then card (rng f) c= meet { (card B1) where B1 is Basis of T : verum } by A18, SETFAM_1:6;
then A23: card (rng f) = meet { (card B1) where B1 is Basis of T : verum } by A19, XBOOLE_0:def 10
.= weight T by WAYBEL23:def 5 ;
A24: dom f = the carrier of T by FUNCT_2:def 1;

now

let x1, x2 be set ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies not x1 <> x2 )
assume that
A25: x1 in dom f and
A26: x2 in dom f and
A27: f . x1 = f . x2 ; :: thesis: not x1 <> x2
reconsider x3 = x1, x4 = x2 as Point of T by A25, A26;
A28: f . x3 = meet { A where A is Element of the topology of T : x3 in A } by A4;
A29: f . x4 = meet { A where A is Element of the topology of T : x4 in A } by A4;
assume x1 <> x2 ; :: thesis: contradiction
then consider V being Subset of T such that
A30: V is open and
A31: ( ( x3 in V & not x4 in V ) or ( x4 in V & not x3 in V ) ) by T_0TOPSP:def 7;

now

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

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

V in the topology of T by A30, PRE_TOPC:def 5;
then A33: V in { A where A is Element of the topology of T : x3 in A } by A32;
A34: meet { A where A is Element of the topology of T : x3 in A } c= V

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in meet { A where A is Element of the topology of T : x3 in A } or z in V )
assume z in meet { A where A is Element of the topology of T : x3 in A } ; :: thesis: z in V
hence z in V by A33, SETFAM_1:def 1; :: thesis: verum

end;

the carrier of T in the topology of T by PRE_TOPC:def 1;
then A35: the carrier of T in { A where A is Element of the topology of T : x4 in A } ;

now

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 consider A being Element of the topology of T such that
A36: Y = A and
A37: x4 in A ;
thus x4 in Y by A36, A37; :: thesis: verum

end;

then x4 in meet { A where A is Element of the topology of T : x3 in A } by A27, A28, A29, A35, SETFAM_1:def 1;
hence contradiction by A32, A34; :: thesis: verum

end;

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

V in the topology of T by A30, PRE_TOPC:def 5;
then A39: V in { A where A is Element of the topology of T : x4 in A } by A38;
A40: meet { A where A is Element of the topology of T : x4 in A } c= V

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in meet { A where A is Element of the topology of T : x4 in A } or z in V )
assume z in meet { A where A is Element of the topology of T : x4 in A } ; :: thesis: z in V
hence z in V by A39, SETFAM_1:def 1; :: thesis: verum

end;

the carrier of T in the topology of T by PRE_TOPC:def 1;
then A41: the carrier of T in { A where A is Element of the topology of T : x3 in A } ;

now

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 consider A being Element of the topology of T such that
A42: Y = A and
A43: x3 in A ;
thus x3 in Y by A42, A43; :: thesis: verum

end;

then x3 in meet { A where A is Element of the topology of T : x4 in A } by A27, A28, A29, A41, SETFAM_1:def 1;
hence contradiction by A38, A40; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

then f is one-to-one by FUNCT_1:def 8;
then the carrier of T, rng f are_equipotent by A24, WELLORD2:def 4;
hence weight T = card the carrier of T by A23, CARD_1:21; :: thesis: verum