let S be Element of QC-Sub-WFF ; :: 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 such that
A1: ( S = Sub_& S1,S2 & S1 `2 = S2 `2 ) by Def27;
S = [((S1 `1 ) '&' (S2 `1 )),(S1 `2 )] by A1, Def21;
then A2: S `1 = (S1 `1 ) '&' (S2 `1 ) by MCART_1:7;
(S1 `1 ) '&' (S2 `1 ) is conjunctive by QC_LANG1:def 19;
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:46;
( (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:5; :: thesis: verum