theorem Th12: :: FINTOPO7:19

for T being non empty TopSpace ex ET being FMT_TopSpace st
( the carrier of T = the carrier of ET & Family_open_set ET = the topology of T )