:: deftheorem defines is_interior_point_of FINTOPO8:def 3 :
for NT being NTopSpace
for A being Subset of NT
for x being Point of NT holds
( x is_interior_point_of A iff A is a_neighborhood of x );