take - 1 ; :: thesis: ( - 1 is negative & - 1 is integer )
thus ( - 1 is negative & - 1 is integer ) ; :: thesis: verum