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