reconsider j = 1 as Element of REAL by NUMBERS:19;
take j ; :: thesis: j is positive
thus j is positive ; :: thesis: verum