let A be QC-alphabet ; for H 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 H is_immediate_constituent_of P ! V
let H be 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 H is_immediate_constituent_of P ! V
let k be 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 P be 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 V be QC-variable_list of k,A; not H is_immediate_constituent_of P ! V
assume A1:
H is_immediate_constituent_of P ! V
; contradiction
A2:
P ! V is atomic
;
then A3:
((@ (P ! V)) . 1) `1 <> 3
by QC_LANG1:19;
A4:
((@ (P ! V)) . 1) `1 <> 2
by A2, QC_LANG1:19;
A5:
for H1 being Element of QC-WFF A holds
( not P ! V = H '&' H1 & not P ! V = H1 '&' H )
by A4, QC_LANG1:18, QC_LANG1:def 20;
'not' H is negative
;
then A6:
((@ ('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
A7:
P ! V = All (z,H)
by A1, A6, A5;
All (z,H) is universal
;
hence
contradiction
by A3, A7, QC_LANG1:18; verum