let p be QC-formula; :: thesis: ( p is atomic implies still_not-bound_in p = still_not-bound_in (the_arguments_of p) )
assume A1: p is atomic ; :: thesis: still_not-bound_in p = still_not-bound_in (the_arguments_of p)
thus H₁(p) = H₂(p) from QC_LANG3:sch 4(Lm1, A1); :: thesis: verum