let H 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 holds not H is_immediate_constituent_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 holds not H is_immediate_constituent_of P ! V
let P be QC-pred_symbol of k; :: thesis: for V being QC-variable_list of holds not H is_immediate_constituent_of P ! V
let V be QC-variable_list of ; :: thesis: not H is_immediate_constituent_of P ! V
assume A1: H is_immediate_constituent_of P ! V ; :: thesis: contradiction
( P ! V is atomic & 'not' H is negative ) by QC_LANG1:def 17, QC_LANG1:def 18;
then A2: ( ((@ (P ! V)) . 1) `1 <> 0 & ((@ (P ! V)) . 1) `1 <> 1 & ((@ (P ! V)) . 1) `1 <> 2 & ((@ (P ! V)) . 1) `1 <> 3 & ((@ ('not' H)) . 1) `1 = 1 ) by QC_LANG1:49, QC_LANG1:50;

now

given H1 being Element of QC-WFF such that A3: ( P ! V = H '&' H1 or P ! V = H1 '&' H ) ; :: thesis: contradiction
( H '&' H1 is conjunctive & H1 '&' H is conjunctive ) by QC_LANG1:def 19;
hence contradiction by A2, A3, QC_LANG1:49; :: thesis: verum

end;

then consider z being bound_QC-variable such that
A4: P ! V = All z,H by A1, A2, Def20;
All z,H is universal by QC_LANG1:def 20;
hence contradiction by A2, A4, QC_LANG1:49; :: thesis: verum