let T be non empty TopSpace; :: thesis:
let B be Basis of T; :: thesis:
let x be Element of T; :: thesis:
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 set ; :: according to TARSKI:def 3 :: thesis:
assume a in { U where U is Subset of T : ( x in U & U in B ) } ; :: thesis:
then ex U being Subset of T st
( a = U & x in U & U in B ) ;
hence a in B ; :: thesis:

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 CANTOR_1:def 2;
hence Bx c= the topology of T by A1, XBOOLE_1:1; :: according to YELLOW_8:def 2 :: thesis:

now

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

end;

hence x in Intersect Bx by SETFAM_1:58; :: thesis:
let S be Subset of T; :: thesis:
assume A2: ( S is open & x in S ) ; :: thesis:
consider V being Subset of T such that
A3: ( V in B & x in V & V c= S ) by A2, YELLOW_9:31;
V in Bx by A3;
hence ex b₁ being Element of K10(the carrier of T) st
( b₁ in Bx & b₁ c= S ) by A3; :: thesis:

end;

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