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