let A be QC-alphabet ; :: thesis: for x being bound_QC-variable of A
for p being QC-formula of A holds still_not-bound_in (Ex (x,p)) = (still_not-bound_in p) \ {x}
let x be bound_QC-variable of A; :: thesis: for p being QC-formula of A holds still_not-bound_in (Ex (x,p)) = (still_not-bound_in p) \ {x}
let p be QC-formula of A; :: thesis: still_not-bound_in (Ex (x,p)) = (still_not-bound_in p) \ {x}
Ex (x,p) = 'not' (All (x,('not' p))) by QC_LANG2:def 5;
hence still_not-bound_in (Ex (x,p)) = still_not-bound_in (All (x,('not' p))) by Th7
.= (still_not-bound_in ('not' p)) \ {x} by Th12
.= (still_not-bound_in p) \ {x} by Th7 ;
:: thesis: verum