theorem Th45: :: SUBLEMMA:45

for Al being QC-alphabet
for p, q being Element of CQC-WFF Al st still_not-bound_in p c= Bound_Vars p & still_not-bound_in q c= Bound_Vars q holds
still_not-bound_in (p '&' q) c= Bound_Vars (p '&' q)