let p be QC-formula; :: thesis: ( p is conjunctive implies still_not-bound_in p = (still_not-bound_in (the_left_argument_of p)) \/ (still_not-bound_in (the_right_argument_of p)) )
assume A1: p is conjunctive ; :: thesis: still_not-bound_in p = (still_not-bound_in (the_left_argument_of p)) \/ (still_not-bound_in (the_right_argument_of p))
for d1, d2 being Subset of bound_QC-variables st d1 = H₁( the_left_argument_of p) & d2 = H₁( the_right_argument_of p) holds
H₁(p) = H₄(d1,d2) from QC_LANG3:sch 6(Lm1, A1);
hence still_not-bound_in p = (still_not-bound_in (the_left_argument_of p)) \/ (still_not-bound_in (the_right_argument_of p)) ; :: thesis: verum