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 A2: x in (seq a,b) \/ {((a + b) + 1)} ; :: thesis: x in seq a,(b + 1)
( x in seq a,b or x in {((a + b) + 1)} ) by A2, 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 A3: x in seq a,(b + 1) ; :: thesis: x in (seq a,b) \/ {((a + b) + 1)}
reconsider x = x as Element of NAT by A3;
( 1 + a <= x & x <= (b + 1) + a ) by A3, Th1;
then ( 1 + a <= x & ( x <= a + b or x = (a + b) + 1 ) ) by NAT_1:8;
then ( x in seq a,b or x in {((a + b) + 1)} ) by TARSKI:def 1;
hence x in (seq a,b) \/ {((a + b) + 1)} by XBOOLE_0:def 3; :: thesis: verum