let T be non empty TopSpace; :: thesis: for x being Point of
for J being Basis of x holds not J is empty
let x be Point of ; :: 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 st
( W in J & W c= [#] T ) by TOPS_1:53, YELLOW_8:22;
hence not J is empty ; :: thesis: verum