let p be QC-formula; :: thesis: ( p is negative implies still_not-bound_in p = still_not-bound_in (the_argument_of p) )
assume A1: p is negative ; :: thesis: still_not-bound_in p = still_not-bound_in (the_argument_of p)
thus H₁(p) = H₃(H₁( the_argument_of p)) from QC_LANG3:sch 5(Lm1, A1); :: thesis: verum