let p, q be QC-formula; :: 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 by QC_LANG1:def 18;
then ( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q ) by QC_LANG1:def 23, QC_LANG1:def 24;
hence still_not-bound_in (p '&' q) = (still_not-bound_in p) \/ (still_not-bound_in q) by A1, Th13; :: thesis: verum