let n, m, k be Nat; :: thesis: (seq (n,m)) \/ (seq ((n + m),k)) = seq (n,(m + k))
A1: seq (n,m) c= seq (n,(m + k))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in seq (n,m) or x in seq (n,(m + k)) )
assume A2: x in seq (n,m) ; :: thesis: x in seq (n,(m + k))
reconsider x = x as Nat by A2;
A3: ( n < x & x <= n + m & n + m <= (n + m) + k ) by A2, Th73, NAT_1:11;
then ( x <= (n + m) + k & (n + m) + k = n + (m + k) ) by XXREAL_0:2;
hence x in seq (n,(m + k)) by A3, Th73; :: thesis: verum

end;

seq ((n + m),k) c= seq (n,(m + k))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in seq ((n + m),k) or x in seq (n,(m + k)) )
assume A4: x in seq ((n + m),k) ; :: thesis: x in seq (n,(m + k))
reconsider x = x as Nat by A4;
A5: ( n <= n + m & n + m < x & x <= (n + m) + k & (n + m) + k = n + (m + k) ) by A4, Th73, NAT_1:11;
then n < x by XXREAL_0:2;
hence x in seq (n,(m + k)) by A5, Th73; :: thesis: verum

end;

then A6: (seq (n,m)) \/ (seq ((n + m),k)) c= seq (n,(m + k)) by A1, XBOOLE_1:8;
seq (n,(m + k)) c= (seq (n,m)) \/ (seq ((n + m),k))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in seq (n,(m + k)) or y in (seq (n,m)) \/ (seq ((n + m),k)) )
assume A7: y in seq (n,(m + k)) ; :: thesis: y in (seq (n,m)) \/ (seq ((n + m),k))
then reconsider y = y as Nat ;
A8: ( n < y & y <= n + (m + k) & n + (m + k) = (n + m) + k ) by A7, Th73;

per cases ( y <= n + m or y > n + m ) ;

suppose y <= n + m ; :: thesis: y in (seq (n,m)) \/ (seq ((n + m),k))

then y in seq (n,m) by A8, Th73;
hence y in (seq (n,m)) \/ (seq ((n + m),k)) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose y > n + m ; :: thesis: y in (seq (n,m)) \/ (seq ((n + m),k))

then y in seq ((n + m),k) by A8, Th73;
hence y in (seq (n,m)) \/ (seq ((n + m),k)) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence (seq (n,m)) \/ (seq ((n + m),k)) = seq (n,(m + k)) by A6, XBOOLE_0:def 10; :: thesis: verum