Let $E_j$ be a D17: Finite set for each $j \in J$ such that
| (i) | $\bigcap_{j \in J} E_j$ is the D76: Set intersection of $\{ E_j \}_{j \in J}$ |
Then $\bigcap_{j \in J} E_j$ is a D17: Finite set.