:: deftheorem defines Int FINTOPO8:def 5 :
for NT being NTopSpace
for A being Subset of NT holds Int A = { x where x is Point of NT : x is_interior_point_of A } ;