let a, b be Nat; :: 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:7;
then A1: seq (a,b) c= seq (a,(b + 1)) by Th4;
let x be object ; :: 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 object ; :: 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