take id NAT ; :: thesis: id NAT is increasing
thus id NAT is increasing ; :: thesis: verum