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