let A be QC-alphabet ; :: thesis: for F being Element of QC-WFF A
for k being Nat
for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds not F is_proper_subformula_of P ! V
let F be Element of QC-WFF A; :: thesis: for k being Nat
for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds not F is_proper_subformula_of P ! V
let k be Nat; :: thesis: for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds not F is_proper_subformula_of P ! V
let P be QC-pred_symbol of k,A; :: thesis: for V being QC-variable_list of k,A holds not F is_proper_subformula_of P ! V
let V be QC-variable_list of k,A; :: 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 A st G is_immediate_constituent_of P ! V by Th55;
hence contradiction by Th42; :: thesis: verum