theorem :: EQREL_1:54

for X being set
for a being Subset-Family of X holds union (union a) = union { (union A) where A is Subset of X : A in a }