theorem :: YELLOW14:21

for T being TopStruct
for x, y being Point of T
for Y, V being Subset of T st Y = {y} & x in Cl Y & V is open & x in V holds
y in V