take n,n --> (- 1) ; :: thesis: ( n,n --> (- 1) is Negative & n,n --> (- 1) is Nonpositive )
thus ( n,n --> (- 1) is Negative & n,n --> (- 1) is Nonpositive ) ; :: thesis: verum