Description: Projective subspace closure, which is the smallest projective subspace
containing an arbitrary set of atoms. The subspace closure of the union
of a set of projective subspaces is their supremum in PSubSp .
Related to an analogous definition of closure used in Lemma 3.1.4 of
PtakPulmannova p. 68. (Note that this closure is not necessarily one
of the closed projective subspaces PSubCl of df-psubclN .)
(Contributed by NM, 7-Sep-2013)