let n, k be Nat; :: thesis: ( n < k implies ((Seg k) \ (Seg (k -' n))) \/ {(k -' n)} = (Seg k) \ (Seg (k -' (n + 1))) )
assume A1: n < k ; :: thesis: ((Seg k) \ (Seg (k -' n))) \/ {(k -' n)} = (Seg k) \ (Seg (k -' (n + 1)))
set Sn1 = (Seg k) \ (Seg (k -' (n + 1)));
set Sn = (Seg k) \ (Seg (k -' n));

now :: thesis: for x being object st x in ((Seg k) \ (Seg (k -' n))) \/ {(k -' n)} holds
x in (Seg k) \ (Seg (k -' (n + 1)))

let x be object ; :: thesis: ( x in ((Seg k) \ (Seg (k -' n))) \/ {(k -' n)} implies b₁ in (Seg k) \ (Seg (k -' (n + 1))) )
assume A2: x in ((Seg k) \ (Seg (k -' n))) \/ {(k -' n)} ; :: thesis: b₁ in (Seg k) \ (Seg (k -' (n + 1)))

per cases ( x in (Seg k) \ (Seg (k -' n)) or x in {(k -' n)} ) by A2, XBOOLE_0:def 3;

suppose A3: x in (Seg k) \ (Seg (k -' n)) ; :: thesis: b₁ in (Seg k) \ (Seg (k -' (n + 1)))

n <= n + 1 by NAT_1:13;
then (Seg k) \ (Seg (k -' n)) c= (Seg k) \ (Seg (k -' (n + 1))) by Th4;
hence x in (Seg k) \ (Seg (k -' (n + 1))) by A3; :: thesis: verum

end;

suppose A4: x in {(k -' n)} ; :: thesis: b₁ in (Seg k) \ (Seg (k -' (n + 1)))

then reconsider y = x as Nat ;
A5: n < n + 1 by NAT_1:13;
n + 1 <= k by A1, NAT_1:13;
then A6: k -' (n + 1) < k -' n by A5, Th2;
A7: x = k -' n by A4, TARSKI:def 1;
then y <= k by NAT_D:35;
hence x in (Seg k) \ (Seg (k -' (n + 1))) by A7, A6, Th3; :: thesis: verum

end;

end;

end;

then A8: ((Seg k) \ (Seg (k -' n))) \/ {(k -' n)} c= (Seg k) \ (Seg (k -' (n + 1))) ;

now :: thesis: for x being object st x in (Seg k) \ (Seg (k -' (n + 1))) holds
x in ((Seg k) \ (Seg (k -' n))) \/ {(k -' n)}

let x be object ; :: thesis: ( x in (Seg k) \ (Seg (k -' (n + 1))) implies b₁ in ((Seg k) \ (Seg (k -' n))) \/ {(k -' n)} )
assume A9: x in (Seg k) \ (Seg (k -' (n + 1))) ; :: thesis: b₁ in ((Seg k) \ (Seg (k -' n))) \/ {(k -' n)}
reconsider y = x as Element of NAT by A9;
A10: y <= k by A9, Th3;
A11: (k -' (n + 1)) + 1 = k -' n by A1, NAT_D:59;
k -' (n + 1) < y by A9, Th3;
then A12: k -' n <= y by A11, NAT_1:13;

per cases ( k -' n = y or k -' n < y ) by A12, XXREAL_0:1;

suppose k -' n = y ; :: thesis: b₁ in ((Seg k) \ (Seg (k -' n))) \/ {(k -' n)}

then y in {(k -' n)} by TARSKI:def 1;
hence x in ((Seg k) \ (Seg (k -' n))) \/ {(k -' n)} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose k -' n < y ; :: thesis: b₁ in ((Seg k) \ (Seg (k -' n))) \/ {(k -' n)}

then y in (Seg k) \ (Seg (k -' n)) by A10, Th3;
hence x in ((Seg k) \ (Seg (k -' n))) \/ {(k -' n)} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

then (Seg k) \ (Seg (k -' (n + 1))) c= ((Seg k) \ (Seg (k -' n))) \/ {(k -' n)} ;
hence ((Seg k) \ (Seg (k -' n))) \/ {(k -' n)} = (Seg k) \ (Seg (k -' (n + 1))) by A8, XBOOLE_0:def 10; :: thesis: verum