set e = the Element of vSUB A;
defpred S1[ object ] means for D being non empty set st D is A -Sub-closed holds
$1 in D;
consider D0 being set such that
A1: for x being object holds
( x in D0 iff ( x in [:([:NAT,(QC-symbols A):] *),(vSUB A):] & S1[x] ) ) from XBOOLE_0:sch 1();
 0 in QC-symbols A by QC_LANG1:3;
then ( [<*[0,0]*>, the Element of vSUB A] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for D being non empty set st D is A -Sub-closed holds
[<*[0,0]*>, the Element of vSUB A] in D ) ) by Lm4;
then reconsider D0 = D0 as non empty set by A1;
take D0 ; :: thesis: ( D0 is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds
D0 c= D ) )
D0 c= [:([:NAT,(QC-symbols A):] *),(vSUB A):] by A1;
hence D0 is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] ; :: according to SUBSTUT1:def 16 :: thesis: ( ( for k being Nat
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in D0 ) & ( for e being Element of vSUB A holds [<*[0,0]*>,e] in D0 ) & ( for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in D0 holds
[(<*[1,0]*> ^ p),e] in D0 ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in D0 & [q,e] in D0 holds
[((<*[2,0]*> ^ p) ^ q),e] in D0 ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 ) & ( for D being non empty set st D is A -Sub-closed holds
D0 c= D ) )
thus for k being Nat
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in D0 :: thesis: ( ( for e being Element of vSUB A holds [<*[0,0]*>,e] in D0 ) & ( for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in D0 holds
[(<*[1,0]*> ^ p),e] in D0 ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in D0 & [q,e] in D0 holds
[((<*[2,0]*> ^ p) ^ q),e] in D0 ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 ) & ( for D being non empty set st D is A -Sub-closed holds
D0 c= D ) )
proof
let k be Nat; :: thesis: for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in D0
let p be QC-pred_symbol of k,A; :: thesis: for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in D0
let ll be QC-variable_list of k,A; :: thesis: for e being Element of vSUB A holds [(<*p*> ^ ll),e] in D0
let e be Element of vSUB A; :: thesis: [(<*p*> ^ ll),e] in D0
( [(<*p*> ^ ll),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for D being non empty set st D is A -Sub-closed holds
[(<*p*> ^ ll),e] in D ) ) by Lm5;
hence [(<*p*> ^ ll),e] in D0 by A1; :: thesis: verum
end;
thus for e being Element of vSUB A holds [<*[0,0]*>,e] in D0 :: thesis: ( ( for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in D0 holds
[(<*[1,0]*> ^ p),e] in D0 ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in D0 & [q,e] in D0 holds
[((<*[2,0]*> ^ p) ^ q),e] in D0 ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 ) & ( for D being non empty set st D is A -Sub-closed holds
D0 c= D ) )
proof
let e be Element of vSUB A; :: thesis: [<*[0,0]*>,e] in D0
0 in QC-symbols A by QC_LANG1:3;
then ( [<*[0,0]*>,e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for D being non empty set st D is A -Sub-closed holds
[<*[0,0]*>,e] in D ) ) by Lm4;
hence [<*[0,0]*>,e] in D0 by A1; :: thesis: verum
end;
thus for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in D0 holds
[(<*[1,0]*> ^ p),e] in D0 :: thesis: ( ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in D0 & [q,e] in D0 holds
[((<*[2,0]*> ^ p) ^ q),e] in D0 ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 ) & ( for D being non empty set st D is A -Sub-closed holds
D0 c= D ) )
proof
let p be FinSequence of [:NAT,(QC-symbols A):]; :: thesis: for e being Element of vSUB A st [p,e] in D0 holds
[(<*[1,0]*> ^ p),e] in D0
let e be Element of vSUB A; :: 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 A -Sub-closed holds
[(<*[1,0]*> ^ p),e] in D
proof
let D be non empty set ; :: thesis: ( D is A -Sub-closed implies [(<*[1,0]*> ^ p),e] in D )
assume A4: D is A -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; :: thesis: verum
end;
0 in QC-symbols A by QC_LANG1:3;
then [1,0] in [:NAT,(QC-symbols A):] by ZFMISC_1:87;
then ( rng <*[1,0]*> = {[1,0]} & {[1,0]} c= [:NAT,(QC-symbols A):] ) by FINSEQ_1:39, ZFMISC_1:31;
then reconsider y = <*[1,0]*> as FinSequence of [:NAT,(QC-symbols A):] by FINSEQ_1:def 4;
y ^ p is FinSequence of [:NAT,(QC-symbols A):] ;
then <*[1,0]*> ^ p in [:NAT,(QC-symbols A):] * by FINSEQ_1:def 11;
then [(<*[1,0]*> ^ p),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] 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,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in D0 & [q,e] in D0 holds
[((<*[2,0]*> ^ p) ^ q),e] in D0 :: thesis: ( ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 ) & ( for D being non empty set st D is A -Sub-closed holds
D0 c= D ) )
proof
let p, q be FinSequence of [:NAT,(QC-symbols A):]; :: thesis: for e being Element of vSUB A st [p,e] in D0 & [q,e] in D0 holds
[((<*[2,0]*> ^ p) ^ q),e] in D0
let e be Element of vSUB A; :: 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 A -Sub-closed holds
[((<*[2,0]*> ^ p) ^ q),e] in D
proof
let D be non empty set ; :: thesis: ( D is A -Sub-closed implies [((<*[2,0]*> ^ p) ^ q),e] in D )
assume A7: D is A -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; :: thesis: verum
end;
0 in QC-symbols A by QC_LANG1:3;
then [2,0] in [:NAT,(QC-symbols A):] by ZFMISC_1:87;
then ( rng <*[2,0]*> = {[2,0]} & {[2,0]} c= [:NAT,(QC-symbols A):] ) by FINSEQ_1:39, ZFMISC_1:31;
then reconsider y = <*[2,0]*> as FinSequence of [:NAT,(QC-symbols A):] by FINSEQ_1:def 4;
(y ^ p) ^ q is FinSequence of [:NAT,(QC-symbols A):] ;
then (<*[2,0]*> ^ p) ^ q in [:NAT,(QC-symbols A):] * by FINSEQ_1:def 11;
then [((<*[2,0]*> ^ p) ^ q),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] 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 of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[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 A -Sub-closed holds
D0 c= D
proof
let x be bound_QC-variable of A; :: thesis: for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D0
let p be FinSequence of [:NAT,(QC-symbols A):]; :: thesis: for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D0
let e be Element of vSUB A; :: thesis: ( [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 implies [((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 )
assume A8: [p,((QSub A) . [((<*[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 A -Sub-closed holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D
proof
let D be non empty set ; :: thesis: ( D is A -Sub-closed implies [((<*[3,0]*> ^ <*x*>) ^ p),e] in D )
assume A10: D is A -Sub-closed ; :: thesis: [((<*[3,0]*> ^ <*x*>) ^ p),e] in D
then [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D by A1, A8;
hence [((<*[3,0]*> ^ <*x*>) ^ p),e] in D by A10; :: thesis: verum
end;
(<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,(QC-symbols A):] by Lm3;
then (<*[3,0]*> ^ <*x*>) ^ p in [:NAT,(QC-symbols A):] * by FINSEQ_1:def 11;
then [((<*[3,0]*> ^ <*x*>) ^ p),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] 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 A -Sub-closed implies D0 c= D )
assume A11: D is A -Sub-closed ; :: thesis: D0 c= D
let x be object ; :: 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