theorem :: YELLOW13:22

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