let p be QC-formula; :: thesis: ( p is universal implies still_not-bound_in p = (still_not-bound_in (the_scope_of p)) \ {(bound_in p)} )
assume A1: p is universal ; :: thesis: still_not-bound_in p = (still_not-bound_in (the_scope_of p)) \ {(bound_in p)}
thus H₁(p) = H₅(p,H₁( the_scope_of p)) from QC_LANG3:sch 7(Lm1, A1); :: thesis: verum