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