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 set ; :: 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:21;
then X = the carrier of T by TDLAT_3:20;
hence a in { the carrier of T} by TARSKI:def 1; :: thesis: verum

end;

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