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

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