let A be QC-alphabet ; :: thesis: for H being Element of QC-WFF A
for k being Element of NAT
for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds not H is_immediate_constituent_of P ! V
let H be Element of QC-WFF A; :: thesis: for k being Element of NAT
for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds not H is_immediate_constituent_of P ! V
let k be Element of NAT ; :: thesis: for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds not H is_immediate_constituent_of P ! V
let P be QC-pred_symbol of k,A; :: thesis: for V being QC-variable_list of k,A holds not H is_immediate_constituent_of P ! V
let V be QC-variable_list of k,A; :: thesis: not H is_immediate_constituent_of P ! V
assume A1: H is_immediate_constituent_of P ! V ; :: thesis: contradiction
A2: P ! V is atomic by QC_LANG1:def 18;
then A3: ((@ (P ! V)) . 1) `1 <> 3 by QC_LANG1:19;
A4: ((@ (P ! V)) . 1) `1 <> 2 by A2, QC_LANG1:19;

A5: now :: thesis: for H1 being Element of QC-WFF A holds
( not P ! V = H '&' H1 & not P ! V = H1 '&' H )

given H1 being Element of QC-WFF A such that A6: ( P ! V = H '&' H1 or P ! V = H1 '&' H ) ; :: thesis: contradiction
( H '&' H1 is conjunctive & H1 '&' H is conjunctive ) by QC_LANG1:def 20;
hence contradiction by A4, A6, QC_LANG1:18; :: thesis: verum

end;

'not' H is negative by QC_LANG1:def 19;
then A7: ((@ ('not' H)) . 1) `1 = 1 by QC_LANG1:18;
((@ (P ! V)) . 1) `1 <> 1 by A2, QC_LANG1:19;
then consider z being bound_QC-variable of A such that
A8: P ! V = All (z,H) by A1, A7, A5, Def19;
All (z,H) is universal by QC_LANG1:def 21;
hence contradiction by A3, A8, QC_LANG1:18; :: thesis: verum