let S be Element of QC-Sub-WFF ; :: 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 ,bound_QC-variables :], SQ being second_Q_comp of B such that
A1: ( S = Sub_All B,SQ & B is quantifiable ) by Def28;
S = [(All (B `2 ),((B `1 ) `1 )),SQ] by A1, Def24;
then A2: S `1 = All (B `2 ),((B `1 ) `1 ) by MCART_1:7;
All (B `2 ),((B `1 ) `1 ) is universal by QC_LANG1:def 20;
then A3: len (@ (the_scope_of (All (B `2 ),((B `1 ) `1 )))) < len (@ (S `1 )) by A2, QC_LANG1:47;
(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:8; :: thesis: verum