let p, q be QC-formula; :: thesis: still_not-bound_in (p 'or' q) = (still_not-bound_in p) \/ (still_not-bound_in q)
( p 'or' q is disjunctive & the_left_disjunct_of (p 'or' q) = p & the_right_disjunct_of (p 'or' q) = q ) by QC_LANG2:45, QC_LANG2:def 10;
hence still_not-bound_in (p 'or' q) = (still_not-bound_in p) \/ (still_not-bound_in q) by Th17; :: thesis: verum