theorem :: YELLOW_9:39

for T being non empty TopSpace
for K being prebasis of T
for x being Point of T
for N being net of T st ( for A being Subset of T st A in K & x in A holds
N is_eventually_in A ) holds
for S being Subset of T st rng (netmap (N,T)) c= S holds
x in Cl S