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