let U be Universe; :: thesis: for X being set st union X is Set of U holds
X is Set of U
let X be set ; :: thesis: ( union X is Set of U implies X is Set of U )
assume union X is Set of U ; :: thesis: X is Set of U
then union X is U -set by Def10;
then X is U -set by Th21;
hence X is Set of U by Def10; :: thesis: verum