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 18;
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:45;
(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:2; :: thesis: verum