theorem Th10: :: STIRL2_1:10

for k, n being Nat st k in Segm n holds
( k <= n - 1 & n - 1 is Element of NAT )