for A, X being set st X in A holds
X c= union A by Lm14;