let p, q be QC-formula; :: thesis: still_not-bound_in (p => q) = (still_not-bound_in p) \/ (still_not-bound_in q)
A1: the_consequent_of (p => q) = q by QC_LANG2:30;
( p => q is conditional & the_antecedent_of (p => q) = p ) by QC_LANG2:30, QC_LANG2:def 11;
hence still_not-bound_in (p => q) = (still_not-bound_in p) \/ (still_not-bound_in q) by A1, Th19; :: thesis: verum