theorem Th3: :: LEXBFS:3

for m, n, k being Nat holds
( m in (Seg k) \ (Seg (k -' n)) iff ( k -' n < m & m <= k ) )