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