for S being Subset-Family of F₁() st S = { X where X is Subset of F₁() : P₁[X] } holds
downarrow (union S) = union { (downarrow X) where X is Subset of F₁() : P₁[X] }