let p, q be Element of HP-WFF ; :: thesis: ( len p < len (p '&' q) & len q < len (p '&' q) )
len (p '&' q) = (len (<*2*> ^ p)) + (len q) by FINSEQ_1:22
.= ((len <*2*>) + (len p)) + (len q) by FINSEQ_1:22
.= (1 + (len p)) + (len q) by FINSEQ_1:39
.= 1 + ((len p) + (len q)) ;
then A1: (len p) + (len q) < len (p '&' q) by XREAL_1:29;
( len p <= (len p) + (len q) & len q <= (len p) + (len q) ) by NAT_1:11;
hence ( len p < len (p '&' q) & len q < len (p '&' q) ) by A1, XXREAL_0:2; :: thesis: verum