let m, n, i 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 Th1;
A3: i <= n by A1, Th1;
i <= i + m by NAT_1:11;
then 1 <= i + m by A2, XXREAL_0:2;
hence i + m in Seg (n + m) by A3, Th1, XREAL_1:7; :: thesis: verum