let F be Element of QC-WFF ; :: thesis: for k being Element of NAT
for P being QC-pred_symbol of k
for V being QC-variable_list of k holds not F is_proper_subformula_of P ! V
let k be Element of NAT ; :: thesis: for P being QC-pred_symbol of k
for V being QC-variable_list of k holds not F is_proper_subformula_of P ! V
let P be QC-pred_symbol of k; :: thesis: for V being QC-variable_list of k holds not F is_proper_subformula_of P ! V
let V be QC-variable_list of k; :: thesis: not F is_proper_subformula_of P ! V
assume F is_proper_subformula_of P ! V ; :: thesis: contradiction
then ex G being Element of QC-WFF st G is_immediate_constituent_of P ! V by Th75;
hence contradiction by Th59; :: thesis: verum