theorem Th86: :: QC_LANG2:86

for A being QC-alphabet
for k being Nat
for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds Subformulae (P ! V) = {(P ! V)}