:: deftheorem Def2 defines quasi_basis CANTOR_1:def 2 :
for X being TopStruct
for F being Subset-Family of X holds
( F is quasi_basis iff the topology of X c= UniCl F );