for X being set
for B being non empty Subset-Family of X st B is cap-closed holds
for x being Element of B st x is_/\-irreducible_in B & x <> X holds
for S being finite Subset-Family of X st S c= B & x = Intersect S holds
x in S