let x, y be R_eal; :: thesis: ( x <= 0 & y <= 0 implies x + y <= 0 )
assume A1: ( x <= 0 & y <= 0 ) ; :: thesis: x + y <= 0
per cases ( x = -infty or x <> -infty ) ;
suppose x = -infty ; :: thesis: x + y <= 0
hence x + y <= 0 by A1, SUPINF_2:def 2; :: thesis: verum
end;
suppose x <> -infty ; :: thesis: x + y <= 0
then reconsider a = x as Real by A1, XXREAL_0:14;
now
per cases ( y = -infty or y <> -infty ) ;
suppose y <> -infty ; :: thesis: x + y <= 0
then reconsider b = y as Real by A1, XXREAL_0:14;
a + b <= 0 + 0 by A1;
hence x + y <= 0 by SUPINF_2:1; :: thesis: verum
end;
end;
end;
hence x + y <= 0 ; :: thesis: verum
end;
end;