theorem Th15: :: HILBERT2:15

for p, q being Element of HP-WFF holds
( len p < len (p '&' q) & len q < len (p '&' q) )