:: deftheorem Def10 defines FMT2TopSpace FINTOPO7:def 16 :
for ET being FMT_TopSpace
for b₂ being strict TopSpace holds
( b₂ = FMT2TopSpace ET iff ( the carrier of b₂ = the carrier of ET & Family_open_set ET = the topology of b₂ ) );