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
set p = the Point of T;
reconsider C = P as basis of the Point of T by Def4;
not C is empty ;
hence not P is empty ; :: thesis: verum