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