let A be QC-alphabet ; :: thesis: for S being Element of QC-Sub-WFF A st S is Sub_universal holds
len (@ ((Sub_the_scope_of S) `1)) < len (@ (S `1))
let S be Element of QC-Sub-WFF A; :: thesis: ( S is Sub_universal implies len (@ ((Sub_the_scope_of S) `1)) < len (@ (S `1)) )
assume S is Sub_universal ; :: thesis: len (@ ((Sub_the_scope_of S) `1)) < len (@ (S `1))
then consider B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):], SQ being second_Q_comp of B such that
A1: ( S = Sub_All (B,SQ) & B is quantifiable ) ;
S = [(All ((B `2),((B `1) `1))),SQ] by A1, Def24;
then A2: S `1 = All ((B `2),((B `1) `1)) ;
All ((B `2),((B `1) `1)) is universal ;
then A3: len (@ (the_scope_of (All ((B `2),((B `1) `1))))) < len (@ (S `1)) by A2, QC_LANG1:16;
(Sub_the_scope_of S) `1 = (B `1) `1 by A1, Th21;
hence len (@ ((Sub_the_scope_of S) `1)) < len (@ (S `1)) by A3, QC_LANG2:7; :: thesis: verum