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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D0 or x in [:NAT ,NAT :] * )
thus ( not x in D0 or x in [:NAT ,NAT :] * ) by A2; :: thesis: verum

end;

hence D0 is Subset of ([:NAT ,NAT :] * ) ; :: according to QC_LANG1:def 9 :: thesis: ( ( 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 D0 ) & <*[0 ,0 ]*> in D0 & ( for p being FinSequence of [:NAT ,NAT :] st p in D0 holds
<*[1,0 ]*> ^ p in D0 ) & ( for p, q being FinSequence of [:NAT ,NAT :] st p in D0 & q in D0 holds
(<*[2,0 ]*> ^ p) ^ q in D0 ) & ( for x being bound_QC-variable
for p being FinSequence of [:NAT ,NAT :] st p in D0 holds
(<*[3,0 ]*> ^ <*x*>) ^ p in D0 ) & ( for D being non empty set st D is QC-closed holds
D0 c= D ) )
thus 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 D0 :: thesis: ( <*[0 ,0 ]*> in D0 & ( for p being FinSequence of [:NAT ,NAT :] st p in D0 holds
<*[1,0 ]*> ^ p in D0 ) & ( for p, q being FinSequence of [:NAT ,NAT :] st p in D0 & q in D0 holds
(<*[2,0 ]*> ^ p) ^ q in D0 ) & ( for x being bound_QC-variable
for p being FinSequence of [:NAT ,NAT :] st p in D0 holds
(<*[3,0 ]*> ^ <*x*>) ^ p in D0 ) & ( for D being non empty set st D is QC-closed holds
D0 c= D ) )

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 D0
let p be QC-pred_symbol of k; :: thesis: for ll being QC-variable_list of k holds <*p*> ^ ll in D0
let ll be QC-variable_list of k; :: thesis: <*p*> ^ ll in D0
<*p*> ^ ll is FinSequence of [:NAT ,NAT :] by Lm2;
then A4: <*p*> ^ ll in [:NAT ,NAT :] * by FINSEQ_1:def 11;
for D being non empty set st D is QC-closed holds
<*p*> ^ ll in D by Def9;
hence <*p*> ^ ll in D0 by A2, A4; :: thesis: verum

end;

thus <*[0 ,0 ]*> in D0 by A2, A1, A3; :: thesis: ( ( for p being FinSequence of [:NAT ,NAT :] st p in D0 holds
<*[1,0 ]*> ^ p in D0 ) & ( for p, q being FinSequence of [:NAT ,NAT :] st p in D0 & q in D0 holds
(<*[2,0 ]*> ^ p) ^ q in D0 ) & ( for x being bound_QC-variable
for p being FinSequence of [:NAT ,NAT :] st p in D0 holds
(<*[3,0 ]*> ^ <*x*>) ^ p in D0 ) & ( for D being non empty set st D is QC-closed holds
D0 c= D ) )
thus for p being FinSequence of [:NAT ,NAT :] st p in D0 holds
<*[1,0 ]*> ^ p in D0 :: thesis: ( ( for p, q being FinSequence of [:NAT ,NAT :] st p in D0 & q in D0 holds
(<*[2,0 ]*> ^ p) ^ q in D0 ) & ( for x being bound_QC-variable
for p being FinSequence of [:NAT ,NAT :] st p in D0 holds
(<*[3,0 ]*> ^ <*x*>) ^ p in D0 ) & ( for D being non empty set st D is QC-closed holds
D0 c= D ) )

proof

reconsider h = <*[1,0 ]*> as FinSequence of [:NAT ,NAT :] by Lm1;
let p be FinSequence of [:NAT ,NAT :]; :: thesis: ( p in D0 implies <*[1,0 ]*> ^ p in D0 )
assume A5: p in D0 ; :: thesis: <*[1,0 ]*> ^ p in D0
A6: for D being non empty set st D is QC-closed holds
<*[1,0 ]*> ^ p in D

proof

let D be non empty set ; :: thesis: ( D is QC-closed implies <*[1,0 ]*> ^ p in D )
assume A7: D is QC-closed ; :: thesis: <*[1,0 ]*> ^ p in D
then p in D by A2, A5;
hence <*[1,0 ]*> ^ p in D by A7, Def9; :: thesis: verum

end;

h ^ p is FinSequence of [:NAT ,NAT :] ;
then <*[1,0 ]*> ^ p in [:NAT ,NAT :] * by FINSEQ_1:def 11;
hence <*[1,0 ]*> ^ p in D0 by A2, A6; :: thesis: verum

end;

thus for p, q being FinSequence of [:NAT ,NAT :] st p in D0 & q in D0 holds
(<*[2,0 ]*> ^ p) ^ q in D0 :: thesis: ( ( for x being bound_QC-variable
for p being FinSequence of [:NAT ,NAT :] st p in D0 holds
(<*[3,0 ]*> ^ <*x*>) ^ p in D0 ) & ( for D being non empty set st D is QC-closed holds
D0 c= D ) )

proof

reconsider h = <*[2,0 ]*> as FinSequence of [:NAT ,NAT :] by Lm1;
let p, q be FinSequence of [:NAT ,NAT :]; :: thesis: ( p in D0 & q in D0 implies (<*[2,0 ]*> ^ p) ^ q in D0 )
assume A8: ( p in D0 & q in D0 ) ; :: thesis: (<*[2,0 ]*> ^ p) ^ q in D0
A9: for D being non empty set st D is QC-closed holds
(<*[2,0 ]*> ^ p) ^ q in D

proof

let D be non empty set ; :: thesis: ( D is QC-closed implies (<*[2,0 ]*> ^ p) ^ q in D )
assume A10: D is QC-closed ; :: thesis: (<*[2,0 ]*> ^ p) ^ q in D
then ( p in D & q in D ) by A2, A8;
hence (<*[2,0 ]*> ^ p) ^ q in D by A10, Def9; :: thesis: verum

end;

(h ^ p) ^ q is FinSequence of [:NAT ,NAT :] ;
then (<*[2,0 ]*> ^ p) ^ q in [:NAT ,NAT :] * by FINSEQ_1:def 11;
hence (<*[2,0 ]*> ^ p) ^ q in D0 by A2, A9; :: thesis: verum

end;

thus for x being bound_QC-variable
for p being FinSequence of [:NAT ,NAT :] st p in D0 holds
(<*[3,0 ]*> ^ <*x*>) ^ p in D0 :: thesis: for D being non empty set st D is QC-closed holds
D0 c= D

proof

let x be bound_QC-variable; :: thesis: for p being FinSequence of [:NAT ,NAT :] st p in D0 holds
(<*[3,0 ]*> ^ <*x*>) ^ p in D0
let p be FinSequence of [:NAT ,NAT :]; :: thesis: ( p in D0 implies (<*[3,0 ]*> ^ <*x*>) ^ p in D0 )
assume A11: p in D0 ; :: thesis: (<*[3,0 ]*> ^ <*x*>) ^ p in D0
A12: for D being non empty set st D is QC-closed holds
(<*[3,0 ]*> ^ <*x*>) ^ p in D

proof

let D be non empty set ; :: thesis: ( D is QC-closed implies (<*[3,0 ]*> ^ <*x*>) ^ p in D )
assume A13: D is QC-closed ; :: thesis: (<*[3,0 ]*> ^ <*x*>) ^ p in D
then p in D by A2, A11;
hence (<*[3,0 ]*> ^ <*x*>) ^ p in D by A13, Def9; :: thesis: verum

end;

(<*[3,0 ]*> ^ <*x*>) ^ p is FinSequence of [:NAT ,NAT :] by Lm3;
then (<*[3,0 ]*> ^ <*x*>) ^ p in [:NAT ,NAT :] * by FINSEQ_1:def 11;
hence (<*[3,0 ]*> ^ <*x*>) ^ p in D0 by A2, A12; :: thesis: verum

end;

let D be non empty set ; :: thesis: ( D is QC-closed implies D0 c= D )
assume A14: D is QC-closed ; :: thesis: D0 c= D
let x be set ; :: 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, A14; :: thesis: verum