Re z in INT by Def1;
hence Re z is integer ; :: thesis: