|.a.| - 1 < 1 - 1 by Def2, XREAL_1:9;
hence |.a.| - 1 is negative ; :: thesis: verum