let A be QC-alphabet ; for t being QC-symbol of A
for p, q being Element of CQC-WFF A
for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
for K being Element of Fin (bound_QC-variables A) st [q,t,K,f] in SepQuadruples p holds
not x. t in f .: (still_not-bound_in q)
let t be QC-symbol of A; for p, q being Element of CQC-WFF A
for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
for K being Element of Fin (bound_QC-variables A) st [q,t,K,f] in SepQuadruples p holds
not x. t in f .: (still_not-bound_in q)
let p, q be Element of CQC-WFF A; for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
for K being Element of Fin (bound_QC-variables A) st [q,t,K,f] in SepQuadruples p holds
not x. t in f .: (still_not-bound_in q)
let f be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); for K being Element of Fin (bound_QC-variables A) st [q,t,K,f] in SepQuadruples p holds
not x. t in f .: (still_not-bound_in q)
let K be Element of Fin (bound_QC-variables A); ( [q,t,K,f] in SepQuadruples p implies not x. t in f .: (still_not-bound_in q) )
assume A1:
[q,t,K,f] in SepQuadruples p
; not x. t in f .: (still_not-bound_in q)
assume
x. t in f .: (still_not-bound_in q)
; contradiction
then
( t < t & t <= t )
by A1, Th42, QC_LANG1:22;
hence
contradiction
by QC_LANG1:25; verum