:: deftheorem defines with_propositional_variables HILBERT2:def 3 :
for D being set holds
( D is with_propositional_variables iff for n being Element of NAT holds prop n in D );