let S be Element of QC-Sub-WFF ; :: 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 such that
A1: S = Sub_not S9 by Def26;
A2: 'not' (S9 `1) is negative by QC_LANG1:def 17;
S `1 = 'not' (S9 `1) by A1, MCART_1:7;
then A3: len (@ (the_argument_of ('not' (S9 `1)))) < len (@ (S `1)) by A2, QC_LANG1:12;
(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