:: deftheorem defines point-filtered TOPGEN_3:def 1 :
for X being set
for B being Subset-Family of X holds
( B is point-filtered iff for x, U1, U2 being set st U1 in B & U2 in B & x in U1 /\ U2 holds
ex U being Subset of X st
( U in B & x in U & U c= U1 /\ U2 ) );