theorem Th5: :: LEXBFS:5

for n, k being Nat st n < k holds
((Seg k) \ (Seg (k -' n))) \/ {(k -' n)} = (Seg k) \ (Seg (k -' (n + 1)))