:: deftheorem Def6 defines CQCSub_the_scope_of SUBLEMMA:def 6 :
for Al being QC-alphabet
for S being Element of CQC-Sub-WFF Al st S is Sub_universal holds
CQCSub_the_scope_of S = Sub_the_scope_of S;