theorem :: SUBSTUT1:6

for A being QC-alphabet
for p being QC-formula of A st p is universal holds
Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} by Lm1;