theorem Th6: :: QC_LANG2:6

for A being QC-alphabet
for p being Element of QC-WFF A st p is universal holds
p = All ((bound_in p),(the_scope_of p))