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