theorem Th28: :: SUBSTUT2:28

for Al being QC-alphabet
for i being Nat
for p being Element of CQC-WFF Al
for F1 being QC-formula of Al
for L being PATH of F1,p st F1 is_subformula_of p & 1 <= i & i <= len L holds
L . i is Element of CQC-WFF Al