take - (1. INT.Ring) ; :: thesis: - (1. INT.Ring) is negative
thus - (1. INT.Ring) is negative ; :: thesis: verum