theorem :: QC_LANG2:27

for A being QC-alphabet
for x, y, z being bound_QC-variable of A
for p being Element of QC-WFF A holds
( All (x,y,z,p) is universal & bound_in (All (x,y,z,p)) = x & the_scope_of (All (x,y,z,p)) = All (y,z,p) ) by Th7;