|.a.| - 1 <= 1 - 1 by Def1, XREAL_1:9;
hence not |.a.| - 1 is positive ; :: thesis: verum