let A be QC-alphabet ; :: thesis: for p being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & x <> y & not y in still_not-bound_in h holds
not y in still_not-bound_in p
let p be Element of CQC-WFF A; :: thesis: for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & x <> y & not y in still_not-bound_in h holds
not y in still_not-bound_in p
let h be QC-formula of A; :: thesis: for x, y being bound_QC-variable of A st p = h . x & x <> y & not y in still_not-bound_in h holds
not y in still_not-bound_in p
let x, y be bound_QC-variable of A; :: thesis: ( p = h . x & x <> y & not y in still_not-bound_in h implies not y in still_not-bound_in p )
assume that
A1: p = h . x and
A2: x <> y and
A3: not y in still_not-bound_in h and
A4: y in still_not-bound_in p ; :: thesis: contradiction
A5: still_not-bound_in p c= (still_not-bound_in h) \/ {x} by A1, Th63;

per cases ( y in still_not-bound_in h or y in {x} ) by A4, A5, XBOOLE_0:def 3;

suppose y in still_not-bound_in h ; :: thesis: contradiction

hence contradiction by A3; :: thesis: verum

end;

suppose y in {x} ; :: thesis: contradiction

hence contradiction by A2, TARSKI:def 1; :: thesis: verum

end;

end;