let T be non empty TopSpace; :: thesis: for p being Point of T
for P being basis of p holds not P is empty
let p be Point of T; :: thesis: for P being basis of p holds not P is empty
let P be basis of p; :: thesis: not P is empty
Int ([#] T) = [#] T by TOPS_1:15;
then ex W being Subset of T st
( W in P & p in Int W & W c= [#] T ) by Def1;
hence not P is empty ; :: thesis: verum