for ET being FMT_TopSpace holds ET = TopSpace2FMT (FMT2TopSpace ET)