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