let T be non empty TopSpace; :: thesis: for p being Point of T
for P being Basis of p holds P is basis of p
let p be Point of T; :: thesis: for P being Basis of p holds P is basis of p
let P be Basis of p; :: thesis: P is basis of p

now

let A be Subset of T; :: thesis: ( p in Int A implies ex V being Subset of T st
( V in P & p in Int V & V c= A ) )
assume p in Int A ; :: thesis: ex V being Subset of T st
( V in P & p in Int V & V c= A )
then consider V being Subset of T such that
A1: ( V in P & V c= Int A ) by YELLOW_8:def 2;
take V = V; :: thesis: ( V in P & p in Int V & V c= A )
A2: Int A c= A by TOPS_1:44;
V is open by A1, YELLOW_8:21;
then Int V = V by TOPS_1:55;
hence ( V in P & p in Int V & V c= A ) by A1, A2, XBOOLE_1:1, YELLOW_8:21; :: thesis: verum

end;

hence P is basis of p by Def1; :: thesis: verum