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 19;
then A3: len (@ (the_scope_of (All ((B `2),((B `1) `1))))) < len (@ (S `1)) by A2, QC_LANG1:14;
(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