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