set X = { S where S is Element of QC-Sub-WFF : P₁[S] } ;
not { S where S is Element of QC-Sub-WFF : P₁[S] } is empty

proof

set e = the Element of vSUB ;
reconsider V = [VERUM, the Element of vSUB ] as Element of QC-Sub-WFF by Def16;
V is Sub_VERUM by Def19;
then P₁[V] by A2;
then V in { S where S is Element of QC-Sub-WFF : P₁[S] } ;
hence not { S where S is Element of QC-Sub-WFF : P₁[S] } is empty ; :: thesis: verum

end;

then reconsider X = { S where S is Element of QC-Sub-WFF : P₁[S] } as non empty set ;
for e being Element of vSUB holds [VERUM,e] in X

proof

let e be Element of vSUB ; :: thesis: [VERUM,e] in X
reconsider V = [VERUM,e] as Element of QC-Sub-WFF by Def16;
V is Sub_VERUM by Def19;
then P₁[V] by A2;
hence [VERUM,e] in X ; :: thesis: verum

end;

then A6: for e being Element of vSUB holds [<*[0,0]*>,e] in X ;
A7: for p being FinSequence of [:NAT,NAT:]
for e being Element of vSUB st [p,e] in X holds
[(<*[1,0]*> ^ p),e] in X

proof

let p be FinSequence of [:NAT,NAT:]; :: thesis: for e being Element of vSUB st [p,e] in X holds
[(<*[1,0]*> ^ p),e] in X
let e be Element of vSUB ; :: 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 such that
A8: S = [p,e] and
A9: P₁[S] ;
P₁[ Sub_not S] by A3, A9;
then A10: Sub_not S in X ;
consider p9 being Element of QC-WFF , e9 being Element of vSUB such that
A11: S = [p9,e9] by Th8;
A12: S `1 = p9 by A11, MCART_1:7;
p = p9 by A8, A11, ZFMISC_1:27;
hence [(<*[1,0]*> ^ p),e] in X by A8, A10, A12, MCART_1:7; :: thesis: verum

end;

A13: 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 X holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in X

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 X holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in X
let p be FinSequence of [:NAT,NAT:]; :: thesis: for e being Element of vSUB st [p,(QSub . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in X holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in X
let e be Element of vSUB ; :: thesis: ( [p,(QSub . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in X implies [((<*[3,0]*> ^ <*x*>) ^ p),e] in X )
assume [p,(QSub . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in X ; :: thesis: [((<*[3,0]*> ^ <*x*>) ^ p),e] in X
then consider S being Element of QC-Sub-WFF such that
A14: S = [p,(QSub . [((<*[3,0]*> ^ <*x*>) ^ p),e])] and
A15: P₁[S] ;
consider B being set such that
A16: B = [S,x] ;
reconsider B = B as Element of [:QC-Sub-WFF,bound_QC-variables:] by A16;
A17: ( B `1 = S & B `2 = x ) by A16, MCART_1:7;
S `1 = p by A14, MCART_1:7;
then A18: S `2 = QSub . [(All (x,(S `1))),e] by A14, MCART_1:7;
then A19: B is quantifiable by A17, Def22;
then reconsider e = e as second_Q_comp of B by A18, A17, Def23;
P<sub>1</sub>[ Sub_All (B,e)] by A5, A15, A16, A19;
then Sub_All (B,e) in X ;
then [(All ((B `2),((B `1) `1))),e] in X by A19, Def24;
hence [((<*[3,0]*> ^ <*x*>) ^ p),e] in X by A14, A17, MCART_1:7; :: thesis: verum

end;

let F be Element of QC-Sub-WFF ; :: thesis: P₁[F]
A20: X c= [:([:NAT,NAT:] *),vSUB:]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in [:([:NAT,NAT:] *),vSUB:] )
assume x in X ; :: thesis: x in [:([:NAT,NAT:] *),vSUB:]
then ex S being Element of QC-Sub-WFF st
( x = S & P₁[S] ) ;
then consider p being Element of QC-WFF , e being Element of vSUB such that
A21: x = [p,e] by Th8;
p = @ p ;
then p in [:NAT,NAT:] * by FINSEQ_1:def 11;
hence x in [:([:NAT,NAT:] *),vSUB:] by A21, ZFMISC_1:def 2; :: thesis: verum

end;

A22: for p, q being FinSequence of [:NAT,NAT:]
for e being Element of vSUB 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,NAT:]; :: thesis: for e being Element of vSUB st [p,e] in X & [q,e] in X holds
[((<*[2,0]*> ^ p) ^ q),e] in X
let e be Element of vSUB ; :: 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 such that
A23: S1 = [p,e] and
A24: P₁[S1] ;
assume [q,e] in X ; :: thesis: [((<*[2,0]*> ^ p) ^ q),e] in X
then consider S2 being Element of QC-Sub-WFF such that
A25: S2 = [q,e] and
A26: P₁[S2] ;
consider p9 being Element of QC-WFF , e1 being Element of vSUB such that
A27: [p,e] = [p9,e1] by A23, Th8;
A28: e = e1 by A27, ZFMISC_1:27;
A29: S1 `2 = e1 by A23, A27, MCART_1:7;
then A30: S1 `2 = S2 `2 by A25, A28, MCART_1:7;
then P<sub>1</sub>[ Sub_& (S1,S2)] by A4, A24, A26;
then Sub_& (S1,S2) in X ;
then A31: [((S1 `1) '&' (S2 `1)),(S1 `2)] in X by A30, Def21;
A32: p = p9 by A27, ZFMISC_1:27;
S1 `1 = p9 by A23, A27, MCART_1:7;
hence [((<*[2,0]*> ^ p) ^ q),e] in X by A25, A32, A28, A29, A31, MCART_1:7; :: thesis: verum

end;

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 X

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 X
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 X
let ll be QC-variable_list of k; :: thesis: for e being Element of vSUB holds [(<*P*> ^ ll),e] in X
let e be Element of vSUB ; :: thesis: [(<*P*> ^ ll),e] in X
( P₁[ 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:6; :: thesis: verum

end;

then X is QC-Sub-closed by A20, A6, A7, A22, A13, Def16;
then QC-Sub-WFF c= X by Def17;
then F in X by TARSKI:def 3;
then ex S being Element of QC-Sub-WFF st
( S = F & P₁[S] ) ;
hence P₁[F] ; :: thesis: verum