let A be QC-alphabet ; :: thesis: 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; :: thesis: 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; :: thesis: 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)); :: thesis: 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); :: thesis: ( [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 ; :: thesis: not x. t in f .: (still_not-bound_in q)

assume x. t in f .: (still_not-bound_in q) ; :: thesis: contradiction

then ( t < t & t <= t ) by A1, Th42, QC_LANG1:22;

hence contradiction by QC_LANG1:25; :: thesis: verum

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; :: thesis: 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; :: thesis: 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)); :: thesis: 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); :: thesis: ( [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 ; :: thesis: not x. t in f .: (still_not-bound_in q)

assume x. t in f .: (still_not-bound_in q) ; :: thesis: contradiction

then ( t < t & t <= t ) by A1, Th42, QC_LANG1:22;

hence contradiction by QC_LANG1:25; :: thesis: verum