let n, i, m be Nat; :: thesis: ( i > 0 & i + m in Seg (n + m) implies ( i in Seg n & i in Seg (n + m) ) )
assume that
A1: i > 0 and
A2: i + m in Seg (n + m) ; :: thesis: ( i in Seg n & i in Seg (n + m) )
1 = 0 + 1 ;
then A3: 1 <= i by A1, NAT_1:13;
A4: i + m <= n + m by A2, Th1;
i <= n by A2, Th1, XREAL_1:6;
hence i in Seg n by A3; :: thesis: i in Seg (n + m)
i <= i + m by NAT_1:11;
then i <= n + m by A4, XXREAL_0:2;
hence i in Seg (n + m) by A3; :: thesis: verum