for n being non trivial Nat holds n < Triangle n