:: deftheorem Def1 defines with_VERUM HILBERT1:def 1 :
for D being set holds
( D is with_VERUM iff <*0*> in D );