theorem :: FINTOPO7:25

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