let T be non empty anti-discrete TopStruct ; :: thesis: for p being Point of T
for D being Basis of holds D = { the carrier of T}
let p be Point of T; :: thesis: for D being Basis of holds D = { the carrier of T}
let D be Basis of ; :: thesis: D = { the carrier of T}
thus D c= { the carrier of T} :: according to XBOOLE_0:def 10 :: thesis: { the carrier of T} c= D

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in D or a in { the carrier of T} )
assume A1: a in D ; :: thesis: a in { the carrier of T}
then reconsider X = a as Subset of T ;
( X is open & p in X ) by A1, YELLOW_8:12;
then X = the carrier of T by TDLAT_3:18;
hence a in { the carrier of T} by TARSKI:def 1; :: thesis: verum

end;

hence { the carrier of T} c= D by ZFMISC_1:33; :: thesis: verum