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 p9 being Element of QC-WFF such that
A8: p = p9 and
A9: P₁[p9] ;
P₁[ All x,p9] 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 p9 being Element of QC-WFF such that
A11: p = p9 and
A12: P₁[p9] ;
assume q in X ; :: thesis: (<*[2,0 ]*> ^ p) ^ q in X
then consider q9 being Element of QC-WFF such that
A13: q = q9 and
A14: P₁[q9] ;
P₁[p9 '&' q9] 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 p9 being Element of QC-WFF such that
A16: p = p9 and
A17: P₁[p9] ;
P₁[ 'not' p9] by A3, A17;
hence <*[1,0 ]*> ^ p in X by A16; :: thesis: verum

end;

let F9 be Element of QC-WFF ; :: thesis: P₁[F9]
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 F9 in X by TARSKI:def 3;
then ex F99 being Element of QC-WFF st
( F9 = F99 & P₁[F99] ) ;
hence P₁[F9] ; :: thesis: verum