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 A1: 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
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
{ A where A is Element of the topology of T : x 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 : 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 consider A being Element of the topology of T such that
A2: z = A and
x in A ;
thus z in bool the carrier of T by A2; :: thesis: verum

end;

then reconsider sfA = { A where A is Element of the topology of T : x 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
A3: P = A and
x in A ;
thus P is open by A3, PRE_TOPC:def 5; :: thesis: verum

end;

then A4: 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 ;
defpred S₁[ set ] means x in $1;
deffunc H₁( set ) -> set = $1;
{ H₁(A) where A is Element of tT : S₁[A] } is finite from PRE_CIRC:sch 1();
then A5: meet sfA is open by A4, TOPS_2:27;
the carrier of T is Element of the topology of T by PRE_TOPC:def 1;
then A6: the carrier of T in sfA ;

now

let Y be set ; :: thesis: ( Y in sfA implies x in Y )
assume Y in sfA ; :: thesis: x in Y
then consider A being Element of the topology of T such that
A7: Y = A and
A8: x in A ;
thus x in Y by A7, A8; :: thesis: verum

end;

then x in meet sfA by A6, SETFAM_1:def 1;
then consider a being Subset of T such that
A9: a in B and
A10: x in a and
A11: a c= meet sfA by A5, YELLOW_9:31;
meet sfA c= a

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in meet sfA or z in a )
assume A12: z in meet sfA ; :: thesis: z in a
B c= the topology of T by CANTOR_1:def 2;
then a in sfA by A9, A10;
hence z in a by A12, SETFAM_1:def 1; :: thesis: verum

end;

hence meet { A where A is Element of the topology of T : x in A } in B by A9, A11, XBOOLE_0:def 10; :: thesis: verum