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