theorem Th23: :: SUBSTUT1:23

for A being QC-alphabet
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)) )