per cases ( x = 0 or x < 0 ) ;

suppose x = 0 ; :: thesis: not x + y is positive

hence x + y <= 0 by Th4; :: according to XXREAL_0:def 6 :: thesis: verum

end;

suppose x < 0 ; :: thesis: not x + y is positive

hence x + y <= 0 by Lm14; :: according to XXREAL_0:def 6 :: thesis: verum

end;

end;