for FMT being non empty FMT_Space_Str ex S being RelStr st
for x being Element of FMT holds U_FMT x is Subset of S