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