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