let n, k, m be Nat; :: thesis: ( n <= m implies (Seg k) \ (Seg (k -' n)) c= (Seg k) \ (Seg (k -' m)) )
assume A1: n <= m ; :: thesis: (Seg k) \ (Seg (k -' n)) c= (Seg k) \ (Seg (k -' m))

per cases ( k < m or m <= k ) ;

suppose k < m ; :: thesis: (Seg k) \ (Seg (k -' n)) c= (Seg k) \ (Seg (k -' m))

then A2: Seg (k -' m) = {} by FINSEQ_1:4, NAT_2:10;
for x being set st x in (Seg k) \ (Seg (k -' n)) holds
x in Seg k by XBOOLE_0:def 5;
hence (Seg k) \ (Seg (k -' n)) c= (Seg k) \ (Seg (k -' m)) by A2, TARSKI:def 3; :: thesis: verum

end;

suppose A3: m <= k ; :: thesis: (Seg k) \ (Seg (k -' n)) c= (Seg k) \ (Seg (k -' m))

now

let x be set ; :: thesis: ( x in (Seg k) \ (Seg (k -' n)) implies b₁ in (Seg k) \ (Seg (k -' m)) )
assume A4: x in (Seg k) \ (Seg (k -' n)) ; :: thesis: b₁ in (Seg k) \ (Seg (k -' m))
reconsider y = x as Element of NAT by A4;
A5: ( k -' n < y & y <= k ) by A4, Th5;

per cases ( m = n or n < m ) by A1, XXREAL_0:1;

suppose m = n ; :: thesis: b₁ in (Seg k) \ (Seg (k -' m))

hence x in (Seg k) \ (Seg (k -' m)) by A4; :: thesis: verum

end;

suppose n < m ; :: thesis: b₁ in (Seg k) \ (Seg (k -' m))

then k -' m < k -' n by A3, Th2;
then ( k -' m < y & y <= k ) by A5, XXREAL_0:2;
hence x in (Seg k) \ (Seg (k -' m)) by Th5; :: thesis: verum

end;

end;

end;

hence (Seg k) \ (Seg (k -' n)) c= (Seg k) \ (Seg (k -' m)) by TARSKI:def 3; :: thesis: verum

end;

end;