consider e being Element of vSUB ;
defpred S₁[ set ] means for D being non empty set st D is QC-Sub-closed holds
$1 in D;
consider D0 being set such that
A1: for x being set holds
( x in D0 iff ( x in [:([:NAT,NAT:] *),vSUB:] & S₁[x] ) ) from XBOOLE_0:sch 1();
( [<*[0,0]*>,e] in [:([:NAT,NAT:] *),vSUB:] & ( for D being non empty set st D is QC-Sub-closed holds
[<*[0,0]*>,e] in D ) ) by Def16, Lm3;
then reconsider D0 = D0 as non empty set by A1;
take D0 ; :: thesis:
D0 c= [:([:NAT,NAT:] *),vSUB:]

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

end;

hence D0 is Subset of [:([:NAT,NAT:] *),vSUB:] ; :: according to SUBSTUT1:def 16 :: thesis:
thus for k being Element of NAT
for p being QC-pred_symbol of k
for ll being QC-variable_list of k
for e being Element of vSUB holds [(<*p*> ^ ll),e] in D0 :: thesis:

let k be Element of NAT ; :: thesis:
let p be QC-pred_symbol of k; :: thesis:
let ll be QC-variable_list of k; :: thesis:
let e be Element of vSUB ; :: thesis:
( [(<*p*> ^ ll),e] in [:([:NAT,NAT:] *),vSUB:] & ( for D being non empty set st D is QC-Sub-closed holds
[(<*p*> ^ ll),e] in D ) ) by Def16, Lm4;
hence [(<*p*> ^ ll),e] in D0 by A1; :: thesis:

end;

thus for e being Element of vSUB holds [<*[0,0]*>,e] in D0 :: thesis:

let e be Element of vSUB ; :: thesis:
( [<*[0,0]*>,e] in [:([:NAT,NAT:] *),vSUB:] & ( for D being non empty set st D is QC-Sub-closed holds
[<*[0,0]*>,e] in D ) ) by Def16, Lm3;
hence [<*[0,0]*>,e] in D0 by A1; :: thesis:

end;

thus for p being FinSequence of [:NAT,NAT:]
for e being Element of vSUB st [p,e] in D0 holds
[(<*[1,0]*> ^ p),e] in D0 :: thesis:

let p be FinSequence of [:NAT,NAT:]; :: thesis:
let e be Element of vSUB ; :: thesis:
assume A2: [p,e] in D0 ; :: thesis:
A3: for D being non empty set st D is QC-Sub-closed holds
[(<*[1,0]*> ^ p),e] in D

let D be non empty set ; :: thesis:
assume A4: D is QC-Sub-closed ; :: thesis:
then [p,e] in D by A1, A2;
hence [(<*[1,0]*> ^ p),e] in D by A4, Def16; :: thesis:

end;

<*[1,0]*> ^ p in [:NAT,NAT:] * by FINSEQ_1:def 11;
then [(<*[1,0]*> ^ p),e] in [:([:NAT,NAT:] *),vSUB:] by ZFMISC_1:def 2;
hence [(<*[1,0]*> ^ p),e] in D0 by A1, A3; :: thesis:

end;

thus for p, q being FinSequence of [:NAT,NAT:]
for e being Element of vSUB st [p,e] in D0 & [q,e] in D0 holds
[((<*[2,0]*> ^ p) ^ q),e] in D0 :: thesis:

let p, q be FinSequence of [:NAT,NAT:]; :: thesis:
let e be Element of vSUB ; :: thesis:
assume A5: ( [p,e] in D0 & [q,e] in D0 ) ; :: thesis:
A6: for D being non empty set st D is QC-Sub-closed holds
[((<*[2,0]*> ^ p) ^ q),e] in D

let D be non empty set ; :: thesis:
assume A7: D is QC-Sub-closed ; :: thesis:
then ( [p,e] in D & [q,e] in D ) by A1, A5;
hence [((<*[2,0]*> ^ p) ^ q),e] in D by A7, Def16; :: thesis:

end;

(<*[2,0]*> ^ p) ^ q in [:NAT,NAT:] * by FINSEQ_1:def 11;
then [((<*[2,0]*> ^ p) ^ q),e] in [:([:NAT,NAT:] *),vSUB:] by ZFMISC_1:def 2;
hence [((<*[2,0]*> ^ p) ^ q),e] in D0 by A1, A6; :: thesis:

end;

thus for x being bound_QC-variable
for p being FinSequence of [:NAT,NAT:]
for e being Element of vSUB st [p,(QSub . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 :: thesis:

let x be bound_QC-variable; :: thesis:
let p be FinSequence of [:NAT,NAT:]; :: thesis:
let e be Element of vSUB ; :: thesis:
assume A8: [p,(QSub . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 ; :: thesis:
A9: for D being non empty set st D is QC-Sub-closed holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D

let D be non empty set ; :: thesis:
assume A10: D is QC-Sub-closed ; :: thesis:
then [p,(QSub . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D by A1, A8;
hence [((<*[3,0]*> ^ <*x*>) ^ p),e] in D by A10, Def16; :: thesis:

end;

(<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,NAT:] by Lm2;
then (<*[3,0]*> ^ <*x*>) ^ p in [:NAT,NAT:] * by FINSEQ_1:def 11;
then [((<*[3,0]*> ^ <*x*>) ^ p),e] in [:([:NAT,NAT:] *),vSUB:] by ZFMISC_1:def 2;
hence [((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 by A1, A9; :: thesis:

end;

let D be non empty set ; :: thesis:
assume A11: D is QC-Sub-closed ; :: thesis:
let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in D0 ; :: thesis:
hence x in D by A1, A11; :: thesis: