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

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

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;

assume that
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