let U be Universe; :: thesis: for X being Set of U holds union X is Set of U
let X be Set of U; :: thesis: union X is Set of U
X is U -set by Def10;
then union X is U -set by CLASSES2:59;
hence union X is Set of U by Def10; :: thesis: verum