let T be non empty TopSpace; :: thesis: for x being Point of T
for B being Basis of x holds B <> {}
let x be Point of T; :: thesis: for B being Basis of x holds B <> {}
let B be Basis of x; :: thesis: B <> {}
A1: the carrier of T in the topology of T by PRE_TOPC:def 1;
set U1 = [#] T;
reconsider T = T as non empty TopStruct ;
[#] T is open by A1, PRE_TOPC:def 2;
then ex U2 being Subset of T st
( U2 in B & U2 c= [#] T ) by YELLOW_8:13;
hence B <> {} ; :: thesis: verum