:: deftheorem defines open FINTOPO7:def 14 :
for ET being FMT_TopSpace
for S being Subset-Family of ET holds
( S is open iff S c= Family_open_set ET );