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