let A be QC-alphabet ; :: thesis: for S being Element of QC-Sub-WFF A st S is Sub_conjunctive holds
( len (@ ((Sub_the_left_argument_of S) `1)) < len (@ (S `1)) & len (@ ((Sub_the_right_argument_of S) `1)) < len (@ (S `1)) )
let S be Element of QC-Sub-WFF A; :: thesis: ( S is Sub_conjunctive implies ( len (@ ((Sub_the_left_argument_of S) `1)) < len (@ (S `1)) & len (@ ((Sub_the_right_argument_of S) `1)) < len (@ (S `1)) ) )
assume S is Sub_conjunctive ; :: thesis: ( len (@ ((Sub_the_left_argument_of S) `1)) < len (@ (S `1)) & len (@ ((Sub_the_right_argument_of S) `1)) < len (@ (S `1)) )
then consider S1, S2 being Element of QC-Sub-WFF A such that
A1: ( S = Sub_& (S1,S2) & S1 `2 = S2 `2 ) ;
S = [((S1 `1) '&' (S2 `1)),(S1 `2)] by A1, Def21;
then A2: S `1 = (S1 `1) '&' (S2 `1) ;
(S1 `1) '&' (S2 `1) is conjunctive ;
then A3: ( len (@ (the_left_argument_of ((S1 `1) '&' (S2 `1)))) < len (@ (S `1)) & len (@ (the_right_argument_of ((S1 `1) '&' (S2 `1)))) < len (@ (S `1)) ) by A2, QC_LANG1:15;
( (Sub_the_right_argument_of S) `1 = S2 `1 & (Sub_the_left_argument_of S) `1 = S1 `1 ) by A1, Th18, Th19;
hence ( len (@ ((Sub_the_left_argument_of S) `1)) < len (@ (S `1)) & len (@ ((Sub_the_right_argument_of S) `1)) < len (@ (S `1)) ) by A3, QC_LANG2:4; :: thesis: verum