:: deftheorem Def9 defines TopSpace2FMT FINTOPO7:def 15 :
for T being non empty TopSpace
for b₂ being FMT_TopSpace holds
( b₂ = TopSpace2FMT T iff ( the carrier of b₂ = the carrier of T & Family_open_set b₂ = the topology of T ) );