:: deftheorem Def1 defines with_FALSUM INTPRO_1:def 1 :
for E being set holds
( E is with_FALSUM iff <*0*> in E );