let a, b be Nat; (seq (a,b)) \/ {((a + b) + 1)} = seq (a,(b + 1))
thus
(seq (a,b)) \/ {((a + b) + 1)} c= seq (a,(b + 1))
XBOOLE_0:def 10 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 ;
TARSKI:def 3 ( 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)}
;
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;
verum
end;
let x be object ; TARSKI:def 3 ( not x in seq (a,(b + 1)) or x in (seq (a,b)) \/ {((a + b) + 1)} )
assume A2:
x in seq (a,(b + 1))
; 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; verum