not a + (- b) is heavy ;
hence not a - b is heavy ; :: thesis: verum