:: deftheorem Def8 defines quasi_basis FINTOPO7:def 13 :
for ET being FMT_TopSpace
for F being Subset-Family of ET holds
( F is quasi_basis iff Family_open_set ET c= UniCl F );