theorem :: FINTOPO2:23

for FMT being non empty FMT_Space_Str
for x being Element of FMT
for A being Subset of FMT holds
( x in A ^Fon iff ( x in A & ( for V being Subset of FMT st V in U_FMT x holds
V \ {x} meets A ) ) )