theorem :: YELLOW13:21

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