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

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