:: deftheorem defines Family_open_set FINTOPO7:def 11 :
for ET being FMT_TopSpace holds Family_open_set ET = { O where O is open Subset of ET : verum } ;