:: deftheorem Def3 defines FamUnion-closed CLASSES3:def 3 :
for X being set holds
( X is FamUnion-closed iff for Y being set
for f being Function st dom f = Y & rng f c= X & Y in X holds
union (rng f) in X );