:: deftheorem Def5 defines with_int_propositional_variables INTPRO_1:def 5 :
for E being set holds
( E is with_int_propositional_variables iff for n being Element of NAT holds <*(5 + (2 * n))*> in E );