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)}

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

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

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)} )
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;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

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