theorem :: FINTOPO8:7

for NT being NTopSpace
for A being Subset of NT
for a being Point of NT holds
( a is_interior_point_of A iff ex O being open Subset of NT st
( a in O & O c= A ) ) by Lm4;