:: deftheorem Def2 defines union-closed CLASSES3:def 2 :
for X being set holds
( X is union-closed iff for Y being set st Y in X holds
union Y in X );