let i, j, n be Nat; :: thesis: ( i < j & j in Segm n implies i in Segm n )
assume that
A1: i < j and
A2: j in Segm n ; :: thesis: i in Segm n
j < n by A2, NAT_1:44;
then i < n by A1, XXREAL_0:2;
hence i in Segm n by NAT_1:44; :: thesis: verum