let r be Real; :: thesis: r < |.r.| + 1
r + 0 < |.r.| + 1 by XREAL_1:8, ABSVALUE:4;
hence r < |.r.| + 1 ; :: thesis: verum