thus ( D is with_propositional_variables implies for n being Element of NAT holds prop n in D ) ; :: thesis: ( ( for n being Element of NAT holds prop n in D ) implies D is with_propositional_variables )
assume A1: for n being Element of NAT holds prop n in D ; :: thesis: D is with_propositional_variables
let n be Element of NAT ; :: according to HILBERT1:def 4 :: thesis: <*(3 + n)*> in D
prop n = <*(3 + n)*> ;
hence <*(3 + n)*> in D by A1; :: thesis: verum