theorem :: SUBSTUT1:3

for A being QC-alphabet
for p being QC-formula of A st p is atomic holds
Bound_Vars p = Bound_Vars (the_arguments_of p) by Lm1;