deffunc H_{1}( set ) -> set = $1;

let T be non empty TopSpace; :: thesis: ( T is finite implies for B being Basis of T

for x being Element of T holds meet { A where A is Element of the topology of T : x in A } in B )

assume T is finite ; :: thesis: for B being Basis of T

for x being Element of T holds meet { A where A is Element of the topology of T : x in A } in B

then reconsider tT = the topology of T as non empty finite set ;

let B be Basis of T; :: thesis: for x being Element of T holds meet { A where A is Element of the topology of T : x in A } in B

let x be Element of T; :: thesis: meet { A where A is Element of the topology of T : x in A } in B

defpred S_{1}[ set ] means x in $1;

{ A where A is Element of the topology of T : x in A } c= bool the carrier of T

reconsider sfA = sfA as Subset-Family of T ;

then the carrier of T in sfA ;

then A2: x in meet sfA by A1, SETFAM_1:def 1;

_{1}(A) where A is Element of tT : S_{1}[A] } is finite
from PRE_CIRC:sch 1();

then meet sfA is open by A3, TOPS_2:20, TOPS_2:def 1;

then consider a being Subset of T such that

A4: a in B and

A5: x in a and

A6: a c= meet sfA by A2, YELLOW_9:31;

meet sfA c= a

let T be non empty TopSpace; :: thesis: ( T is finite implies for B being Basis of T

for x being Element of T holds meet { A where A is Element of the topology of T : x in A } in B )

assume T is finite ; :: thesis: for B being Basis of T

for x being Element of T holds meet { A where A is Element of the topology of T : x in A } in B

then reconsider tT = the topology of T as non empty finite set ;

let B be Basis of T; :: thesis: for x being Element of T holds meet { A where A is Element of the topology of T : x in A } in B

let x be Element of T; :: thesis: meet { A where A is Element of the topology of T : x in A } in B

defpred S

{ A where A is Element of the topology of T : x in A } c= bool the carrier of T

proof

then reconsider sfA = { A where A is Element of the topology of T : x in A } as Subset-Family of T ;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { A where A is Element of the topology of T : x in A } or z in bool the carrier of T )

assume z in { A where A is Element of the topology of T : x in A } ; :: thesis: z in bool the carrier of T

then ex A being Element of the topology of T st

( z = A & x in A ) ;

hence z in bool the carrier of T ; :: thesis: verum

end;assume z in { A where A is Element of the topology of T : x in A } ; :: thesis: z in bool the carrier of T

then ex A being Element of the topology of T st

( z = A & x in A ) ;

hence z in bool the carrier of T ; :: thesis: verum

reconsider sfA = sfA as Subset-Family of T ;

A1: now :: thesis: for Y being set st Y in sfA holds

x in Y

the carrier of T is Element of the topology of T
by PRE_TOPC:def 1;x in Y

let Y be set ; :: thesis: ( Y in sfA implies x in Y )

assume Y in sfA ; :: thesis: x in Y

then ex A being Element of the topology of T st

( Y = A & x in A ) ;

hence x in Y ; :: thesis: verum

end;assume Y in sfA ; :: thesis: x in Y

then ex A being Element of the topology of T st

( Y = A & x in A ) ;

hence x in Y ; :: thesis: verum

then the carrier of T in sfA ;

then A2: x in meet sfA by A1, SETFAM_1:def 1;

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

P is open

{ HP 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 & x in A ) ;

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

end;assume P in sfA ; :: thesis: P is open

then ex A being Element of the topology of T st

( P = A & x in A ) ;

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

then meet sfA is open by A3, TOPS_2:20, TOPS_2:def 1;

then consider a being Subset of T such that

A4: a in B and

A5: x in a and

A6: a c= meet sfA by A2, YELLOW_9:31;

meet sfA c= a

proof

hence
meet { A where A is Element of the topology of T : x in A } in B
by A4, A6, XBOOLE_0:def 10; :: thesis: verum
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in meet sfA or z in a )

B c= the topology of T by TOPS_2:64;

then a in sfA by A4, A5;

hence ( not z in meet sfA or z in a ) by SETFAM_1:def 1; :: thesis: verum

end;B c= the topology of T by TOPS_2:64;

then a in sfA by A4, A5;

hence ( not z in meet sfA or z in a ) by SETFAM_1:def 1; :: thesis: verum