reconsider i = id NAT as Real_Sequence by FUNCT_2:7, NUMBERS:19;
take i ; :: thesis: ( i is increasing & i is natural-valued )
thus ( i is increasing & i is natural-valued ) ; :: thesis: verum