let p, q be Element of HP-WFF ; :: thesis: ( len p < len (p => q) & len q < len (p => q) )
len (p => q) = (len (<*1*> ^ p)) + (len q) by FINSEQ_1:22
.= ((len <*1*>) + (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