:: deftheorem Def9 defines Intersect SETFAM_1:def 9 :
for M being set
for B being Subset-Family of M holds
( ( B <> {} implies Intersect B = meet B ) & ( not B <> {} implies Intersect B = M ) );