theorem Th22: :: FINTOPO2:22

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