let A be QC-alphabet ; for S being Element of QC-Sub-WFF A ex p being QC-formula of A ex e being Element of vSUB A st S = [p,e]
let S be Element of QC-Sub-WFF A; ex p being QC-formula of A ex e being Element of vSUB A st S = [p,e]
( [:(QC-WFF A),(vSUB A):] is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( 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 [:(QC-WFF A),(vSUB A):] ) & ( for e being Element of vSUB A holds [<*[0,0]*>,e] in [:(QC-WFF A),(vSUB A):] ) & ( for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] holds
[(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):] ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] & [q,e] in [:(QC-WFF A),(vSUB A):] holds
[((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):] ) & ( 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 [:(QC-WFF A),(vSUB A):] holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):] ) )
by Th7;
then
[:(QC-WFF A),(vSUB A):] is A -Sub-closed
;
then
QC-Sub-WFF A c= [:(QC-WFF A),(vSUB A):]
by Def17;
then
S in [:(QC-WFF A),(vSUB A):]
;
then consider a, b being object such that
A1:
a in QC-WFF A
and
A2:
b in vSUB A
and
A3:
S = [a,b]
by ZFMISC_1:def 2;
reconsider e = b as Element of vSUB A by A2;
reconsider p = a as Element of QC-WFF A by A1;
take
p
; ex e being Element of vSUB A st S = [p,e]
take
e
; S = [p,e]
thus
S = [p,e]
by A3; verum