take n,n --> 1 ; :: thesis: ( n,n --> 1 is Positive & n,n --> 1 is Nonnegative )
thus ( n,n --> 1 is Positive & n,n --> 1 is Nonnegative ) ; :: thesis: verum