theorem Th10: :: SUBSTUT2:10

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for Sub being CQC_Substitution of Al
for S being Element of CQC-Sub-WFF Al st S `2 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) & S `1 = p holds
( [S,x] is quantifiable & ex S1 being Element of CQC-Sub-WFF Al st S1 = [(All (x,p)),Sub] )