set X = { S where S is Element of QC-Sub-WFF F1() : P1[S] } ;
not { S where S is Element of QC-Sub-WFF F1() : P1[S] } is empty
proof
set e = the Element of vSUB F1();
reconsider V = [(VERUM F1()), the Element of vSUB F1()] as Element of QC-Sub-WFF F1() by Def16;
V is F1() -Sub_VERUM ;
then P1[V] by A2;
then V in { S where S is Element of QC-Sub-WFF F1() : P1[S] } ;
hence not { S where S is Element of QC-Sub-WFF F1() : P1[S] } is empty ; :: thesis: verum
end;
then reconsider X = { S where S is Element of QC-Sub-WFF F1() : P1[S] } as non empty set ;
for e being Element of vSUB F1() holds [(VERUM F1()),e] in X
proof
let e be Element of vSUB F1(); :: thesis: [(VERUM F1()),e] in X
reconsider V = [(VERUM F1()),e] as Element of QC-Sub-WFF F1() by Def16;
V is F1() -Sub_VERUM ;
then P1[V] by A2;
hence [(VERUM F1()),e] in X ; :: thesis: verum
end;
then A6: for e being Element of vSUB F1() holds [<*[0,0]*>,e] in X ;
A7: for p being FinSequence of [:NAT,(QC-symbols F1()):]
for e being Element of vSUB F1() st [p,e] in X holds
[(<*[1,0]*> ^ p),e] in X
proof
let p be FinSequence of [:NAT,(QC-symbols F1()):]; :: thesis: for e being Element of vSUB F1() st [p,e] in X holds
[(<*[1,0]*> ^ p),e] in X
let e be Element of vSUB F1(); :: thesis: ( [p,e] in X implies [(<*[1,0]*> ^ p),e] in X )
assume [p,e] in X ; :: thesis: [(<*[1,0]*> ^ p),e] in X
then consider S being Element of QC-Sub-WFF F1() such that
A8: S = [p,e] and
A9: P1[S] ;
 P1[ Sub_not S] by A3, A9;
then Sub_not S in X ;
hence [(<*[1,0]*> ^ p),e] in X by A8; :: thesis: verum
end;
A10: for x being bound_QC-variable of F1()
for p being FinSequence of [:NAT,(QC-symbols F1()):]
for e being Element of vSUB F1() st [p,((QSub F1()) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in X holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in X
proof
let x be bound_QC-variable of F1(); :: thesis: for p being FinSequence of [:NAT,(QC-symbols F1()):]
for e being Element of vSUB F1() st [p,((QSub F1()) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in X holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in X
let p be FinSequence of [:NAT,(QC-symbols F1()):]; :: thesis: for e being Element of vSUB F1() st [p,((QSub F1()) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in X holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in X
let e be Element of vSUB F1(); :: thesis: ( [p,((QSub F1()) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in X implies [((<*[3,0]*> ^ <*x*>) ^ p),e] in X )
assume [p,((QSub F1()) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in X ; :: thesis: [((<*[3,0]*> ^ <*x*>) ^ p),e] in X
then consider S being Element of QC-Sub-WFF F1() such that
A11: S = [p,((QSub F1()) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] and
A12: P1[S] ;
consider B being set such that
A13: B = [S,x] ;
reconsider B = B as Element of [:(QC-Sub-WFF F1()),(bound_QC-variables F1()):] by A13;
A14: ( B `1 = S & B `2 = x ) by A13;
A15: S `2 = (QSub F1()) . [(All (x,(S `1))),e] by A11;
then A16: B is quantifiable by A14;
then reconsider e = e as second_Q_comp of B by A15, A14, Def23;
P1[ Sub_All (B,e)] by A5, A12, A13, A16;
then Sub_All (B,e) in X ;
then [(All ((B `2),((B `1) `1))),e] in X by A16, Def24;
hence [((<*[3,0]*> ^ <*x*>) ^ p),e] in X by A11, A14; :: thesis: verum
end;
let F be Element of QC-Sub-WFF F1(); :: thesis: P1[F]
A17: X c= [:([:NAT,(QC-symbols F1()):] *),(vSUB F1()):]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in [:([:NAT,(QC-symbols F1()):] *),(vSUB F1()):] )
assume x in X ; :: thesis: x in [:([:NAT,(QC-symbols F1()):] *),(vSUB F1()):]
then ex S being Element of QC-Sub-WFF F1() st
( x = S & P1[S] ) ;
then consider p being Element of QC-WFF F1(), e being Element of vSUB F1() such that
A18: x = [p,e] by Th8;
p = @ p ;
then p in [:NAT,(QC-symbols F1()):] * by FINSEQ_1:def 11;
hence x in [:([:NAT,(QC-symbols F1()):] *),(vSUB F1()):] by A18, ZFMISC_1:def 2; :: thesis: verum
end;
A19: for p, q being FinSequence of [:NAT,(QC-symbols F1()):]
for e being Element of vSUB F1() st [p,e] in X & [q,e] in X holds
[((<*[2,0]*> ^ p) ^ q),e] in X
proof
let p, q be FinSequence of [:NAT,(QC-symbols F1()):]; :: thesis: for e being Element of vSUB F1() st [p,e] in X & [q,e] in X holds
[((<*[2,0]*> ^ p) ^ q),e] in X
let e be Element of vSUB F1(); :: thesis: ( [p,e] in X & [q,e] in X implies [((<*[2,0]*> ^ p) ^ q),e] in X )
assume [p,e] in X ; :: thesis: ( not [q,e] in X or [((<*[2,0]*> ^ p) ^ q),e] in X )
then consider S1 being Element of QC-Sub-WFF F1() such that
A20: S1 = [p,e] and
A21: P1[S1] ;
assume [q,e] in X ; :: thesis: [((<*[2,0]*> ^ p) ^ q),e] in X
then consider S2 being Element of QC-Sub-WFF F1() such that
A22: S2 = [q,e] and
A23: P1[S2] ;
consider p9 being Element of QC-WFF F1(), e1 being Element of vSUB F1() such that
A24: [p,e] = [p9,e1] by A20, Th8;
A25: e = e1 by A24, XTUPLE_0:1;
then A26: S1 `2 = e1 by A20;
then A27: S1 `2 = S2 `2 by A22, A25;
then P1[ Sub_& (S1,S2)] by A4, A21, A23;
then Sub_& (S1,S2) in X ;
then A28: [((S1 `1) '&' (S2 `1)),(S1 `2)] in X by A27, Def21;
A29: p = p9 by A24, XTUPLE_0:1;
then S1 `1 = p9 by A20;
hence [((<*[2,0]*> ^ p) ^ q),e] in X by A22, A29, A25, A26, A28; :: thesis: verum
end;
for k being Nat
for P being QC-pred_symbol of k,F1()
for ll being QC-variable_list of k,F1()
for e being Element of vSUB F1() holds [(<*P*> ^ ll),e] in X
proof
let k be Nat; :: thesis: for P being QC-pred_symbol of k,F1()
for ll being QC-variable_list of k,F1()
for e being Element of vSUB F1() holds [(<*P*> ^ ll),e] in X
let P be QC-pred_symbol of k,F1(); :: thesis: for ll being QC-variable_list of k,F1()
for e being Element of vSUB F1() holds [(<*P*> ^ ll),e] in X
let ll be QC-variable_list of k,F1(); :: thesis: for e being Element of vSUB F1() holds [(<*P*> ^ ll),e] in X
let e be Element of vSUB F1(); :: thesis: [(<*P*> ^ ll),e] in X
( P1[ Sub_P (P,ll,e)] & [(P ! ll),e] = Sub_P (P,ll,e) ) by A1, Th9;
then [(P ! ll),e] in X ;
hence [(<*P*> ^ ll),e] in X by QC_LANG1:8; :: thesis: verum
end;
then X is F1() -Sub-closed by A17, A6, A7, A19, A10;
then QC-Sub-WFF F1() c= X by Def17;
then F in X ;
then ex S being Element of QC-Sub-WFF F1() st
( S = F & P1[S] ) ;
hence P1[F] ; :: thesis: verum