:: deftheorem defines with_VERUM HILBERT2:def 2 :
for D being set holds
( D is with_VERUM iff VERUM in D );