let p, q be Element of HP-WFF ; :: thesis: ( p => q <> p & p => q <> q )
( len p < len (p => q) & len q < len (p => q) ) by Th16;
hence ( p => q <> p & p => q <> q ) ; :: thesis: verum