Description: The set of projective subspaces is compactly atomistic: if an atom is in
the projective subspace closure of a set of atoms, it also belongs to
the projective subspace closure of a finite subset of that set.
Analogous to Lemma 3.3.10 of PtakPulmannova p. 74. (Contributed by NM, 10-Sep-2013)(New usage is discouraged.)