thus ( IncAddr (I,k) is initial & IncAddr (I,k) is NAT -defined ) ; :: thesis: verum