let i, n, m be Nat; :: thesis: ( i in Seg n implies i + m in Seg (n + m) )
assume A1: i in Seg n ; :: thesis: i + m in Seg (n + m)
then A2: 1 <= i by Th3;
A3: i <= n by A1, Th3;
i <= i + m by NAT_1:11;
then A4: 1 <= i + m by A2, XXREAL_0:2;
i + m <= n + m by A3, XREAL_1:9;
hence i + m in Seg (n + m) by A4, Th3; :: thesis: verum