let k be natural number ; :: thesis: - 1 < k
- 1 < 0 ;
hence - 1 < k ; :: thesis: verum