VERUM in { F where F is Element of QC-WFF : P₁[F] } by A2;
then reconsider X = { F where F is Element of QC-WFF : P₁[F] } as non empty set ;
A6: for k being Element of NAT
for P being QC-pred_symbol of k
for ll being QC-variable_list of k holds <*P*> ^ ll in X

proof

let k be Element of NAT ; :: thesis: for P being QC-pred_symbol of k
for ll being QC-variable_list of k holds <*P*> ^ ll in X
let P be QC-pred_symbol of k; :: thesis: for ll being QC-variable_list of k holds <*P*> ^ ll in X
let ll be QC-variable_list of k; :: thesis: <*P*> ^ ll in X
P₁[P ! ll] by A1;
then P ! ll in X ;
hence <*P*> ^ ll in X by Th23; :: thesis: verum

end;

A7: for x being bound_QC-variable
for p being FinSequence of [:NAT ,NAT :] st p in X holds
(<*[3,0 ]*> ^ <*x*>) ^ p in X

proof

let x be bound_QC-variable; :: thesis: for p being FinSequence of [:NAT ,NAT :] st p in X holds
(<*[3,0 ]*> ^ <*x*>) ^ p in X
let p be FinSequence of [:NAT ,NAT :]; :: thesis: ( p in X implies (<*[3,0 ]*> ^ <*x*>) ^ p in X )
assume p in X ; :: thesis: (<*[3,0 ]*> ^ <*x*>) ^ p in X
then consider p' being Element of QC-WFF such that
A8: p = p' and
A9: P₁[p'] ;
P₁[ All x,p'] by A5, A9;
hence (<*[3,0 ]*> ^ <*x*>) ^ p in X by A8; :: thesis: verum

end;

A10: for p, q being FinSequence of [:NAT ,NAT :] st p in X & q in X holds
(<*[2,0 ]*> ^ p) ^ q in X

proof

let p, q be FinSequence of [:NAT ,NAT :]; :: thesis: ( p in X & q in X implies (<*[2,0 ]*> ^ p) ^ q in X )
assume p in X ; :: thesis: ( not q in X or (<*[2,0 ]*> ^ p) ^ q in X )
then consider p' being Element of QC-WFF such that
A11: p = p' and
A12: P₁[p'] ;
assume q in X ; :: thesis: (<*[2,0 ]*> ^ p) ^ q in X
then consider q' being Element of QC-WFF such that
A13: q = q' and
A14: P₁[q'] ;
P₁[p' '&' q'] by A4, A12, A14;
hence (<*[2,0 ]*> ^ p) ^ q in X by A11, A13; :: thesis: verum

end;

A15: for p being FinSequence of [:NAT ,NAT :] st p in X holds
<*[1,0 ]*> ^ p in X

proof

let p be FinSequence of [:NAT ,NAT :]; :: thesis: ( p in X implies <*[1,0 ]*> ^ p in X )
assume p in X ; :: thesis: <*[1,0 ]*> ^ p in X
then consider p' being Element of QC-WFF such that
A16: p = p' and
A17: P₁[p'] ;
P₁[ 'not' p'] by A3, A17;
hence <*[1,0 ]*> ^ p in X by A16; :: thesis: verum

end;

let F' be Element of QC-WFF ; :: thesis: P₁[F']
A18: X c= [:NAT ,NAT :] *

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in [:NAT ,NAT :] * )
assume x in X ; :: thesis: x in [:NAT ,NAT :] *
then consider p being Element of QC-WFF such that
A19: x = p and
P₁[p] ;
p = @ p ;
hence x in [:NAT ,NAT :] * by A19, FINSEQ_1:def 11; :: thesis: verum

end;

<*[0 ,0 ]*> in X by A2;
then X is QC-closed by A18, A6, A15, A10, A7, Def9;
then QC-WFF c= X by Def10;
then F' in X by TARSKI:def 3;
then ex F'' being Element of QC-WFF st
( F' = F'' & P₁[F''] ) ;
hence P₁[F'] ; :: thesis: verum