:: deftheorem Def4 defines quasi_prebasis CANTOR_1:def 4 :
for X being TopStruct
for F being Subset-Family of X holds
( F is quasi_prebasis iff ex G being Basis of X st G c= FinMeetCl F );