let T be non empty TopSpace; :: thesis: for p being Point of T
for P being Basis of holds P is basis of p
let p be Point of T; :: thesis: for P being Basis of holds P is basis of p
let P be Basis of ; :: thesis: P is basis of p
now :: thesis: for A being Subset of T st p in Int A holds
ex V being Subset of T st
( V in P & p in Int V & V c= A )
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 and
A2: V c= Int A by YELLOW_8:def 1;
take V = V; :: thesis: ( V in P & p in Int V & V c= A )
V is open by A1, YELLOW_8:12;
then ( Int A c= A & Int V = V ) by TOPS_1:16, TOPS_1:23;
hence ( V in P & p in Int V & V c= A ) by A1, A2, YELLOW_8:12; :: thesis: verum
end;
hence P is basis of p by Def1; :: thesis: verum