theorem :: YELLOW13:14

for T being non empty anti-discrete TopStruct
for p being Point of T
for D being Basis of holds D = { the carrier of T}