A1: <*0*> in NAT * by FINSEQ_1:def 11;
defpred S₁[ set ] means for D being set st D is PL-closed holds
$1 in D;
consider D0 being set such that
A2: for x being set holds
( x in D0 iff ( x in NAT * & S₁[x] ) ) from XFAMILY:sch 1();
A3: for D being set st D is PL-closed holds
<*0*> in D by INTPRO_1:def 1;
then reconsider D0 = D0 as non empty set by A2, A1;
take D0 ; :: thesis: ( D0 is PL-closed & ( for D being set st D is PL-closed holds
D0 c= D ) )
A4: D0 c= NAT * by A2;
for p, q being FinSequence st p in D0 & q in D0 holds
(<*1*> ^ p) ^ q in D0

proof

let p, q be FinSequence; :: thesis: ( p in D0 & q in D0 implies (<*1*> ^ p) ^ q in D0 )
assume that
A5: p in D0 and
A6: q in D0 ; :: thesis: (<*1*> ^ p) ^ q in D0
A7: q in NAT * by A2, A6;
A8: for D being set st D is PL-closed holds
(<*1*> ^ p) ^ q in D

proof

let D be set ; :: thesis: ( D is PL-closed implies (<*1*> ^ p) ^ q in D )
assume A9: D is PL-closed ; :: thesis: (<*1*> ^ p) ^ q in D
then A10: q in D by A2, A6;
p in D by A2, A5, A9;
hence (<*1*> ^ p) ^ q in D by A9, A10, HILBERT1:def 2; :: thesis: verum

end;

p in NAT * by A2, A5;
then reconsider p9 = p, q9 = q as FinSequence of NAT by A7, FINSEQ_1:def 11;
(<*1*> ^ p9) ^ q9 in NAT * by FINSEQ_1:def 11;
hence (<*1*> ^ p) ^ q in D0 by A2, A8; :: thesis: verum

end;

then A11: D0 is with_implication by HILBERT1:def 2;
for n being Element of NAT holds <*(3 + n)*> in D0

proof

let n be Element of NAT ; :: thesis: <*(3 + n)*> in D0
set p = 3 + n;
reconsider h = <*(3 + n)*> as FinSequence of NAT ;
A19: h in NAT * by FINSEQ_1:def 11;
for D being set st D is PL-closed holds
<*(3 + n)*> in D by Def4;
hence <*(3 + n)*> in D0 by A2, A19; :: thesis: verum

end;

then A20: D0 is with_propositional_variables ;
D0 is with_FALSUM by A2, A1, A3;
hence D0 is PL-closed by A4, A20, A11; :: thesis: for D being set st D is PL-closed holds
D0 c= D
let D be set ; :: thesis: ( D is PL-closed implies D0 c= D )
assume A21: D is PL-closed ; :: thesis: D0 c= D
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D0 or x in D )
assume x in D0 ; :: thesis: x in D
hence x in D by A2, A21; :: thesis: verum