reconsider b = - c as positive light Real ;
A2: |.b.| < 1 by Def2;
|.a.| < 1 by Def2;
then ( a - b < 1 - b & 1 - b <= 1 - 0 ) by XREAL_1:9, XREAL_1:10;
then A3: a - b < 1 by XXREAL_0:2;
A4: ( b - a < 1 - a & 1 - a <= 1 - 0 ) by A2, XREAL_1:9, XREAL_1:10;

per cases ( a - b >= 0 or a - b < 0 ) ;

suppose a - b >= 0 ; :: thesis: a + c is light

hence a + c is light by A3, ABSVALUE:def 1; :: thesis: verum

end;

suppose a - b < 0 ; :: thesis: a + c is light

then |.(a - b).| = - (a - b) by ABSVALUE:def 1;
hence a + c is light by A4, XXREAL_0:2; :: thesis: verum

end;

end;