let a, b be natural number ; :: thesis: (seq a,b) \/ {((a + b) + 1)} = seq a,(b + 1)
thus (seq a,b) \/ {((a + b) + 1)} c= seq a,(b + 1) :: according to XBOOLE_0:def 10 :: thesis: seq a,(b + 1) c= (seq a,b) \/ {((a + b) + 1)}

proof

b + 0 <= b + 1 by XREAL_1:9;
then A1: seq a,b c= seq a,(b + 1) by Th4;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (seq a,b) \/ {((a + b) + 1)} or x in seq a,(b + 1) )
assume x in (seq a,b) \/ {((a + b) + 1)} ; :: thesis: x in seq a,(b + 1)
then ( x in seq a,b or x in {((a + b) + 1)} ) by XBOOLE_0:def 3;
then ( x in seq a,(b + 1) or x = a + (b + 1) ) by A1, TARSKI:def 1;
hence x in seq a,(b + 1) by Th3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in seq a,(b + 1) or x in (seq a,b) \/ {((a + b) + 1)} )
assume A2: x in seq a,(b + 1) ; :: thesis: x in (seq a,b) \/ {((a + b) + 1)}
reconsider x = x as Element of NAT by A2;
x <= (b + 1) + a by A2, Th1;
then A3: ( x <= a + b or x = (a + b) + 1 ) by NAT_1:8;
1 + a <= x by A2, Th1;
then ( x in seq a,b or x in {((a + b) + 1)} ) by A3, TARSKI:def 1;
hence x in (seq a,b) \/ {((a + b) + 1)} by XBOOLE_0:def 3; :: thesis: verum