:: deftheorem def4 defines quasi_basis CARDFIL2:def 11 :
for X being set
for B being Subset-Family of X holds
( B is quasi_basis iff for b1, b2 being Element of B ex b being Element of B st b c= b1 /\ b2 );