I `1 in NAT by MCART_1:10;
hence InsCode I is natural ; :: thesis: verum