for FT being non empty filled RelStr holds { (U_FT x) where x is Element of FT : verum } is Cover of FT