for FMT being non empty FMT_Space_Str
for x being Element of FMT
for A being Subset of FMT holds
( x in A ^Foi iff ex V being Subset of FMT st
( V in U_FMT x & V c= A ) )