let p be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable holds still_not-bound_in p c= (still_not-bound_in (All x,p)) \/ {x}
let x be bound_QC-variable; :: 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:16, XBOOLE_1:39;
hence still_not-bound_in p c= (still_not-bound_in (All x,p)) \/ {x} by XBOOLE_1:7; :: thesis: verum