let x, y be R_eal; :: thesis: ( 0 <= x & 0 <= y implies 0 <= x + y )
assume A1: ( 0 <= x & 0 <= y ) ; :: thesis: 0 <= x + y

per cases ( x = +infty or x <> +infty ) ;

suppose x = +infty ; :: thesis: 0 <= x + y

hence 0 <= x + y by A1, SUPINF_2:def 2; :: thesis: verum

end;

suppose x <> +infty ; :: thesis: 0 <= x + y

then reconsider a = x as Real by A1, XXREAL_0:14;

now

per cases ( y = +infty or y <> +infty ) ;

suppose y = +infty ; :: thesis: 0 <= x + y

hence 0 <= x + y by A1, SUPINF_2:def 2; :: thesis: verum

end;

suppose y <> +infty ; :: thesis: 0 <= x + y

then reconsider b = y as Real by A1, XXREAL_0:14;
0 + 0 <= a + b by A1;
hence 0 <= x + y by SUPINF_2:1; :: thesis: verum

end;

end;

end;

hence 0 <= x + y ; :: thesis: verum

end;

end;