let T be non empty TopSpace; :: thesis: for x being Point of T
for J being Basis of x holds not J is empty
let x be Point of T; :: thesis: for J being Basis of x holds not J is empty
let J be Basis of x; :: thesis: not J is empty
ex W being Subset of T st
( W in J & W c= [#] T ) by YELLOW_8:13;
hence not J is empty ; :: thesis: verum