Abstract away facts about "closed under finitary union/intersection"

[Columbus240]

Write a lemma in ZornsLemma of the form:

forall (X : Type) (fam : Family X),
  In fam Full_set /\ (forall U V, In fam U -> In fam V -> In fam (Intersection U V)) <->
  (forall (fin_fam : Family X), Included fin_fam fam -> Finite fin_fam -> In fam (FamilyIntersection fin_fam))

and one for union:

forall (X : Type) (fam : Family X),
  In fam Empty_set /\ (forall U V, In fam U -> In fam V -> In fam (Union U V)) <->
  (forall (fin_fam : Family X), Included fin_fam fam -> Finite fin_fam -> In fam (FamilyUnion fin_fam))

Applications for these lemmas arise/arose in the facts about filters and about open/closed sets. I already have these proofs, but I still need to rebase them.

I think, there’s some further generalization hiding in there... But that is probably not useful.