let A be QC-alphabet ; :: thesis: for S being Element of QC-Sub-WFF A st S is Sub_negative holds
len (@ ((Sub_the_argument_of S) `1)) < len (@ (S `1))
let S be Element of QC-Sub-WFF A; :: thesis: ( S is Sub_negative implies len (@ ((Sub_the_argument_of S) `1)) < len (@ (S `1)) )
assume S is Sub_negative ; :: thesis: len (@ ((Sub_the_argument_of S) `1)) < len (@ (S `1))
then consider S9 being Element of QC-Sub-WFF A such that
A1: S = Sub_not S9 ;
A2: 'not' (S9 `1) is negative ;
S `1 = 'not' (S9 `1) by A1;
then A3: len (@ (the_argument_of ('not' (S9 `1)))) < len (@ (S `1)) by A2, QC_LANG1:14;
(Sub_the_argument_of S) `1 = S9 `1 by A1, Def30;
hence len (@ ((Sub_the_argument_of S) `1)) < len (@ (S `1)) by A3, QC_LANG2:1; :: thesis: verum