take - jj ; :: thesis: - jj is negative
thus - jj is negative by XXREAL_0:def 7; :: thesis: verum