theorem :: SUBSTUT1:5

for A being QC-alphabet
for p being QC-formula of A st p is conjunctive holds
Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) by Lm1;