let m, n, k be Nat; :: thesis: ( m in (Seg k) \ (Seg (k -' n)) iff ( k -' n < m & m <= k ) )

A4: k -' n < m and

A5: m <= k ; :: thesis: m in (Seg k) \ (Seg (k -' n))

0 + 1 <= m by A4, NAT_1:13;

then A6: m in Seg k by A5, FINSEQ_1:1;

not m in Seg (k -' n) by A4, FINSEQ_1:1;

hence m in (Seg k) \ (Seg (k -' n)) by A6, XBOOLE_0:def 5; :: thesis: verum

hereby :: thesis: ( k -' n < m & m <= k implies m in (Seg k) \ (Seg (k -' n)) )

assume that assume A1:
m in (Seg k) \ (Seg (k -' n))
; :: thesis: ( k -' n < m & m <= k )

then A2: not m in Seg (k -' n) by XBOOLE_0:def 5;

A3: m in Seg k by A1, XBOOLE_0:def 5;

then 1 <= m by FINSEQ_1:1;

hence ( k -' n < m & m <= k ) by A3, A2, FINSEQ_1:1; :: thesis: verum

end;then A2: not m in Seg (k -' n) by XBOOLE_0:def 5;

A3: m in Seg k by A1, XBOOLE_0:def 5;

then 1 <= m by FINSEQ_1:1;

hence ( k -' n < m & m <= k ) by A3, A2, FINSEQ_1:1; :: thesis: verum

A4: k -' n < m and

A5: m <= k ; :: thesis: m in (Seg k) \ (Seg (k -' n))

0 + 1 <= m by A4, NAT_1:13;

then A6: m in Seg k by A5, FINSEQ_1:1;

not m in Seg (k -' n) by A4, FINSEQ_1:1;

hence m in (Seg k) \ (Seg (k -' n)) by A6, XBOOLE_0:def 5; :: thesis: verum