let A be QC-alphabet ; :: thesis: for p, q being QC-formula of A holds still_not-bound_in (p '&' q) = (still_not-bound_in p) \/ (still_not-bound_in q)
let p, q be QC-formula of A; :: thesis: still_not-bound_in (p '&' q) = (still_not-bound_in p) \/ (still_not-bound_in q)
set pq = p '&' q;
A1: p '&' q is conjunctive ;
then ( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q ) by QC_LANG1:def 25, QC_LANG1:def 26;
hence still_not-bound_in (p '&' q) = (still_not-bound_in p) \/ (still_not-bound_in q) by A1, Th9; :: thesis: verum