theorem Th8: :: SUBSTUT1:8

for A being 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]