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 A2: k < m ; :: thesis: (Seg k) \ (Seg (k -' n)) c= (Seg k) \ (Seg (k -' m))

A3: for x being object st x in (Seg k) \ (Seg (k -' n)) holds
x in Seg k by XBOOLE_0:def 5;
k -' m = 0 by A2, NAT_2:8;
then Seg (k -' m) = {} ;
hence (Seg k) \ (Seg (k -' n)) c= (Seg k) \ (Seg (k -' m)) by A3; :: thesis: verum

end;

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

now :: thesis: for x being object st x in (Seg k) \ (Seg (k -' n)) holds
x in (Seg k) \ (Seg (k -' m))

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

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 A5; :: thesis: verum

end;

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

then k -' m < k -' n by A4, Th2;
then A7: k -' m < y by A6, XXREAL_0:2;
y <= k by A5, Th3;
hence x in (Seg k) \ (Seg (k -' m)) by A7, Th3; :: thesis: verum

end;

end;

end;

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

end;

end;