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();
consider e being Element of vSUB ;
A2: [<*[0 ,0 ]*>,e] in [:([:NAT ,NAT :] * ),vSUB :] by Lm3;
for D being non empty set st D is QC-Sub-closed holds
[<*[0 ,0 ]*>,e] in D by Def16;
then reconsider D0 = D0 as non empty set by A1, A2;
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
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 ; :: 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:
A3: [<*[0 ,0 ]*>,e] in [:([:NAT ,NAT :] * ),vSUB :] by Lm3;
for D being non empty set st D is QC-Sub-closed holds
[<*[0 ,0 ]*>,e] in D by Def16;
hence [<*[0 ,0 ]*>,e] in D0 by A1, A3; :: 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 A4: [p,e] in D0 ; :: thesis:
<*[1,0 ]*> ^ p in [:NAT ,NAT :] * by FINSEQ_1:def 11;
then A5: [(<*[1,0 ]*> ^ p),e] in [:([:NAT ,NAT :] * ),vSUB :] by ZFMISC_1:def 2;
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 A6: D is QC-Sub-closed ; :: thesis:
then [p,e] in D by A1, A4;
hence [(<*[1,0 ]*> ^ p),e] in D by A6, Def16; :: thesis:

end;

hence [(<*[1,0 ]*> ^ p),e] in D0 by A1, A5; :: 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 A7: ( [p,e] in D0 & [q,e] in D0 ) ; :: thesis:
(<*[2,0 ]*> ^ p) ^ q in [:NAT ,NAT :] * by FINSEQ_1:def 11;
then A8: [((<*[2,0 ]*> ^ p) ^ q),e] in [:([:NAT ,NAT :] * ),vSUB :] by ZFMISC_1:def 2;
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 A9: D is QC-Sub-closed ; :: thesis:
then ( [p,e] in D & [q,e] in D ) by A1, A7;
hence [((<*[2,0 ]*> ^ p) ^ q),e] in D by A9, Def16; :: thesis:

end;

hence [((<*[2,0 ]*> ^ p) ^ q),e] in D0 by A1, A8; :: 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 A10: [p,(QSub . [((<*[3,0 ]*> ^ <*x*>) ^ p),e])] in D0 ; :: thesis:
(<*[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 A11: [((<*[3,0 ]*> ^ <*x*>) ^ p),e] in [:([:NAT ,NAT :] * ),vSUB :] by ZFMISC_1:def 2;
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 A12: D is QC-Sub-closed ; :: thesis:
then [p,(QSub . [((<*[3,0 ]*> ^ <*x*>) ^ p),e])] in D by A1, A10;
hence [((<*[3,0 ]*> ^ <*x*>) ^ p),e] in D by A12, Def16; :: thesis:

end;

hence [((<*[3,0 ]*> ^ <*x*>) ^ p),e] in D0 by A1, A11; :: thesis:

end;

let D be non empty set ; :: thesis:
assume A13: 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, A13; :: thesis: