:: deftheorem defines union-closed ROUGHS_4:def 3 :
for X being set
for F being Subset-Family of X holds
( F is union-closed iff for a being Subset-Family of X st a c= F holds
union a in F );