let k be natural number ; :: thesis: - 1 < k
( - 1 < 0 & 0 <= k ) ;
hence - 1 < k ; :: thesis: verum