let U be Universe; :: thesis: for X being class of U holds union X is class of U
let X be class of U; :: thesis: union X is class of U
A1: not union X is empty

proof

assume union X is empty ; :: thesis: contradiction
then A2: X is U -set by Th45;
X is U -Class by Def12;
hence contradiction by A2; :: thesis: verum

end;

A3: X is U -Class by Def12;
then union X c= union U by ZFMISC_1:77;
then ( union X c= U & not union X in U ) by A3, Th21, CLASSES4:81;
then union X is U -Class ;
hence union X is class of U by A1, Def12; :: thesis: verum