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