let ET be FMT_TopSpace; :: thesis: ET = TopSpace2FMT (FMT2TopSpace ET)
( FMT2TopSpace ET is strict TopSpace & the carrier of (FMT2TopSpace ET) = the carrier of ET & Family_open_set ET = the topology of (FMT2TopSpace ET) ) by Def10;
hence ET = TopSpace2FMT (FMT2TopSpace ET) by Def9; :: thesis: verum