:: deftheorem Def1 defines disjoint_with_NAT FREEALG:def 1 :
for IT being set holds
( IT is disjoint_with_NAT iff IT misses NAT );