let a, b be odd Integer; :: thesis: ( Parity (a + 1) = Parity (b - 1) implies a <> b )
1 is odd ;
hence ( Parity (a + 1) = Parity (b - 1) implies a <> b ) by PSD; :: thesis: verum