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