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