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