deffunc H1( 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 S1[ set ] means x in $1;
{ A where A is Element of the topology of T : x 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 : 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;
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 ;
A1: now :: thesis: for Y being set st Y in sfA holds
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;
the carrier of T is Element of the topology of T by PRE_TOPC:def 1;
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
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;
{ H1(A) where A is Element of tT : S1[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
proof
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;
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