let T be non empty TopSpace; :: thesis: for P being Basis of T
for p being Point of T holds { A where A is Subset of T : ( A in P & p in A ) } is Basis of
let P be Basis of T; :: thesis: for p being Point of T holds { A where A is Subset of T : ( A in P & p in A ) } is Basis of
let p be Point of T; :: thesis: { A where A is Subset of T : ( A in P & p in A ) } is Basis of
set Z = { A where A is Subset of T : ( A in P & p in A ) } ;
{ A where A is Subset of T : ( A in P & p 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 Subset of T : ( A in P & p in A ) } or z in bool the carrier of T )
assume z in { A where A is Subset of T : ( A in P & p in A ) } ; :: thesis: z in bool the carrier of T
then ex A being Subset of T st
( A = z & A in P & p in A ) ;
hence z in bool the carrier of T ; :: thesis: verum

end;

then reconsider Z = { A where A is Subset of T : ( A in P & p in A ) } as Subset-Family of T ;
reconsider Z = Z as Subset-Family of T ;
Z is Basis of

proof

A1: Z is open

proof

let z be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( not z in Z or z is open )
assume z in Z ; :: thesis: z is open
then consider A being Subset of T such that
A2: A = z and
A3: A in P and
p in A ;
A is open by A3, YELLOW_8:10;
hence z is open by A2; :: thesis: verum

end;

Z is p -quasi_basis

proof

now

let z be set ; :: thesis: ( z in Z implies p in z )
assume z in Z ; :: thesis: p in z
then ex A being Subset of T st
( A = z & A in P & p in A ) ;
hence p in z ; :: thesis: verum

end;

hence p in Intersect Z by SETFAM_1:43; :: according to YELLOW_8:def 1 :: thesis: for b₁ being Element of bool the carrier of T holds
( not b₁ is open or not p in b₁ or ex b₂ being Element of bool the carrier of T st
( b₂ in Z & b₂ c= b₁ ) )
let S be Subset of T; :: thesis: ( not S is open or not p in S or ex b₁ being Element of bool the carrier of T st
( b₁ in Z & b₁ c= S ) )
assume ( S is open & p in S ) ; :: thesis: ex b₁ being Element of bool the carrier of T st
( b₁ in Z & b₁ c= S )
then consider V being Subset of T such that
A4: ( V in P & p in V & V c= S ) by YELLOW_9:31;
take V ; :: thesis: ( V in Z & V c= S )
thus ( V in Z & V c= S ) by A4; :: thesis: verum

end;

hence Z is Basis of by A1; :: thesis: verum

end;

hence { A where A is Subset of T : ( A in P & p in A ) } is Basis of ; :: thesis: verum