take -infty ; :: thesis: -infty is negative
thus -infty is negative ; :: thesis: verum