let T be non empty TopSpace; :: thesis: for B being Basis of T
for x being Element of T holds { U where U is Subset of T : ( x in U & U in B ) } is Basis of x
let B be Basis of T; :: thesis: for x being Element of T holds { U where U is Subset of T : ( x in U & U in B ) } is Basis of x
let x be Element of T; :: thesis: { U where U is Subset of T : ( x in U & U in B ) } is Basis of x
set Bx = { U where U is Subset of T : ( x in U & U in B ) } ;
A1: { U where U is Subset of T : ( x in U & U in B ) } c= B

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { U where U is Subset of T : ( x in U & U in B ) } or a in B )
assume a in { U where U is Subset of T : ( x in U & U in B ) } ; :: thesis: a in B
then ex U being Subset of T st
( a = U & x in U & U in B ) ;
hence a in B ; :: thesis: verum

end;

then reconsider Bx = { U where U is Subset of T : ( x in U & U in B ) } as Subset-Family of T by XBOOLE_1:1;
Bx is Basis of x

proof

B c= the topology of T by TOPS_2:64;
then Bx c= the topology of T by A1;
then A2: Bx is open by TOPS_2:64;
Bx is x -quasi_basis

proof

now :: thesis: for a being set st a in Bx holds
x in a

let a be set ; :: thesis: ( a in Bx implies x in a )
assume a in Bx ; :: thesis: x in a
then ex U being Subset of T st
( a = U & x in U & U in B ) ;
hence x in a ; :: thesis: verum

end;

hence x in Intersect Bx by SETFAM_1:43; :: according to YELLOW_8:def 1 :: thesis: for b₁ being Element of K32( the carrier of T) holds
( not b₁ is open or not x in b₁ or ex b₂ being Element of K32( the carrier of T) st
( b₂ in Bx & b₂ c= b₁ ) )
let S be Subset of T; :: thesis: ( not S is open or not x in S or ex b₁ being Element of K32( the carrier of T) st
( b₁ in Bx & b₁ c= S ) )
assume that
A3: S is open and
A4: x in S ; :: thesis: ex b₁ being Element of K32( the carrier of T) st
( b₁ in Bx & b₁ c= S )
consider V being Subset of T such that
A5: V in B and
A6: x in V and
A7: V c= S by A3, A4, YELLOW_9:31;
V in Bx by A5, A6;
hence ex b₁ being Element of K32( the carrier of T) st
( b₁ in Bx & b₁ c= S ) by A7; :: thesis: verum

end;

hence Bx is Basis of x by A2; :: thesis: verum

end;

hence { U where U is Subset of T : ( x in U & U in B ) } is Basis of x ; :: thesis: verum