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