:: deftheorem Def1 defines cup-closed FINSUB_1:def 1 :
for IT being set holds
( IT is cup-closed iff for X, Y being set st X in IT & Y in IT holds
X \/ Y in IT );