take (1,1) --> (- (In (1,REAL))) ; :: thesis: ( (1,1) --> (- (In (1,REAL))) is Negative & (1,1) --> (- (In (1,REAL))) is Nonpositive )
thus ( (1,1) --> (- (In (1,REAL))) is Negative & (1,1) --> (- (In (1,REAL))) is Nonpositive ) ; :: thesis: verum