theorem :: FINTOPO8:8

for NT being NTopSpace
for O being open Subset of NT
for a being Point of NT st a in O holds
a is_interior_point_of O by Lm4;