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

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

hence x + y >= 0 by Tx3; :: according to XXREAL_0:def 7 :: thesis: verum

end;

suppose x > 0 ; :: thesis: not x + y is negative

hence x + y >= 0 by Lm16; :: according to XXREAL_0:def 7 :: thesis: verum

end;

end;