theorem Th15: :: QC_LANG1:15

for A being QC-alphabet
for p being Element of QC-WFF A st p is conjunctive holds
( len (@ (the_left_argument_of p)) < len (@ p) & len (@ (the_right_argument_of p)) < len (@ p) )