let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds still_not-bound_in p c= (still_not-bound_in (All (x,p))) \/ {x}
let p be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al holds still_not-bound_in p c= (still_not-bound_in (All (x,p))) \/ {x}
let x be bound_QC-variable of Al; :: thesis: still_not-bound_in p c= (still_not-bound_in (All (x,p))) \/ {x}
set X = (still_not-bound_in p) \ {x};
( still_not-bound_in (All (x,p)) = (still_not-bound_in p) \ {x} & {x} \/ ((still_not-bound_in p) \ {x}) = {x} \/ (still_not-bound_in p) ) by QC_LANG3:12, XBOOLE_1:39;
hence still_not-bound_in p c= (still_not-bound_in (All (x,p))) \/ {x} by XBOOLE_1:7; :: thesis: verum