let T be non empty anti-discrete TopStruct ; :: thesis: for p being Point of T
for D being correct basis of p holds D = { the carrier of T}
let p be Point of T; :: thesis: for D being correct basis of p holds D = { the carrier of T}
let D be correct basis of p; :: 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 ;
p in Int X by A1, Def3;
then A2: Int X = the carrier of T by TDLAT_3:18;
Int X c= X by TOPS_1:16;
then Int X = X by A2;
hence a in { the carrier of T} by A2, TARSKI:def 1; :: thesis: verum
end;
hence { the carrier of T} c= D by ZFMISC_1:33; :: thesis: verum