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