let T be non empty TopSpace; :: thesis: for P being basis of T holds not P is empty
let P be basis of T; :: thesis: not P is empty
consider p being Point of T;
reconsider C = P as basis of p by Def4;
not C is empty ;
hence not P is empty ; :: thesis: verum