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