:: deftheorem defines is_adherent_point_of FINTOPO8:def 4 :
for NT being NTopSpace
for A being Subset of NT
for x being Point of NT holds
( x is_adherent_point_of A iff for V being Element of U_FMT x holds V meets A );