theorem :: YELLOW13:13

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