take NAT --> the Element of X ; :: thesis: ( NAT --> the Element of X is ascending & NAT --> the Element of X is stagnating )
thus ( NAT --> the Element of X is ascending & NAT --> the Element of X is stagnating ) ; :: thesis: verum