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)
A1: the_right_side_of (p <=> q) = q by QC_LANG2:31;
( p <=> q is biconditional & the_left_side_of (p <=> q) = p ) by QC_LANG2:31, QC_LANG2:def 12;
hence still_not-bound_in (p <=> q) = (still_not-bound_in p) \/ (still_not-bound_in q) by A1, Th17; :: thesis: verum