:: deftheorem Def28 defines the_scope_of QC_LANG1:def 28 :
for A being QC-alphabet
for F being Element of QC-WFF A st F is universal holds
for b₃ being QC-formula of A holds
( b₃ = the_scope_of F iff ex x being bound_QC-variable of A st F = All (x,b₃) );