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