Im z in INT by Def1;
hence Im z is integer ; :: thesis: verum