:: deftheorem Def4 defines with_propositional_variables HILBERT1:def 4 :
for D being set holds
( D is with_propositional_variables iff for n being Element of NAT holds <*(3 + n)*> in D );