let x be bound_QC-variable; :: thesis: for p being Element of QC-WFF
for V being non empty Subset of QC-variables holds Vars (All x,p),V = Vars p,V
let p be Element of QC-WFF ; :: thesis: for V being non empty Subset of QC-variables holds Vars (All x,p),V = Vars p,V
let V be non empty Subset of QC-variables ; :: thesis: Vars (All x,p),V = Vars p,V
A1: All x,p is universal by QC_LANG1:def 20;
then the_scope_of (All x,p) = p by QC_LANG1:def 27;
hence Vars (All x,p),V = Vars p,V by A1, Lm2; :: thesis: verum