theorem Th6: :: FINTOPO7:10

for ET being non empty strict U_FMT_filter FMT_Space_Str
for x being Element of ET holds the carrier of ET in U_FMT x