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 is QC-Sub-closed & ( for D being non empty set st D is QC-Sub-closed holds
D0 c= D ) )
D0 c= [:([:NAT ,NAT :] * ),vSUB :]

proof

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

end;

hence D0 is Subset of [:([:NAT ,NAT :] * ),vSUB :] ; :: according to SUBSTUT1:def 16 :: thesis: ( ( 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 ) & ( for e being Element of vSUB holds [<*[0 ,0 ]*>,e] in D0 ) & ( 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 ) & ( 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 ) & ( 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 ) & ( for D being non empty set st D is QC-Sub-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
for e being Element of vSUB holds [(<*p*> ^ ll),e] in D0 :: thesis: ( ( for e being Element of vSUB holds [<*[0 ,0 ]*>,e] in D0 ) & ( 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 ) & ( 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 ) & ( 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 ) & ( for D being non empty set st D is QC-Sub-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
for e being Element of vSUB holds [(<*p*> ^ ll),e] in D0
let p be QC-pred_symbol of k; :: thesis: for ll being QC-variable_list of k
for e being Element of vSUB holds [(<*p*> ^ ll),e] in D0
let ll be QC-variable_list of k; :: thesis: for e being Element of vSUB holds [(<*p*> ^ ll),e] in D0
let e be Element of vSUB ; :: thesis: [(<*p*> ^ ll),e] in D0
( [(<*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: verum

end;

thus for e being Element of vSUB holds [<*[0 ,0 ]*>,e] in D0 :: thesis: ( ( 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 ) & ( 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 ) & ( 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 ) & ( for D being non empty set st D is QC-Sub-closed holds
D0 c= D ) )

proof

let e be Element of vSUB ; :: thesis: [<*[0 ,0 ]*>,e] in D0
( [<*[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: verum

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: ( ( 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 ) & ( 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 ) & ( for D being non empty set st D is QC-Sub-closed holds
D0 c= D ) )

proof

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

proof

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

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: verum

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: ( ( 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 ) & ( for D being non empty set st D is QC-Sub-closed holds
D0 c= D ) )

proof

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

proof

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

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: verum

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: for D being non empty set st D is QC-Sub-closed holds
D0 c= D

proof

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

proof

let D be non empty set ; :: thesis: ( D is QC-Sub-closed implies [((<*[3,0 ]*> ^ <*x*>) ^ p),e] in D )
assume A10: D is QC-Sub-closed ; :: thesis: [((<*[3,0 ]*> ^ <*x*>) ^ p),e] in D
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: verum

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: verum

end;

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