let U be Universe; :: thesis: for X being set st union X in U holds
X in U
let X be set ; :: thesis: ( union X in U implies X in U )
assume union X in U ; :: thesis: X in U
then A1: bool (union X) in U by CLASSES2:59;
X c= bool (union X) by ZFMISC_1:82;
hence X in U by A1, CLASSES4:13; :: thesis: verum