theorem Th1: :: PENCIL_4:1

for k, n being Nat st k < n & 3 <= n & not k + 1 < n holds
2 <= k