let m, n be Element of NAT ; :: thesis: seq (m,n) c= Seg (m + n)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in seq (m,n) or x in Seg (m + n) )
A1: 1 <= 1 + m by NAT_1:11;
assume A2: x in seq (m,n) ; :: thesis: x in Seg (m + n)
then reconsider x = x as Element of NAT ;
1 + m <= x by A2, Th1;
then A3: 1 <= x by A1, XXREAL_0:2;
x <= n + m by A2, Th1;
hence x in Seg (m + n) by A3, FINSEQ_1:1; :: thesis: verum