let x, y be R_eal; :: thesis: ( ( ( x <= 0. & y < 0. ) or ( x < 0. & y <= 0. ) ) implies x + y < 0. )
assume A1: ( ( x <= 0. & y < 0. ) or ( 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.

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

end;

suppose y <> -infty ; :: thesis: x + y < 0.

then reconsider b = y as Real by A1, XXREAL_0:14;
( ( a <= 0 & b < 0 ) or ( a < 0 & b <= 0 ) )

proof

now

per cases ( ( x <= 0. & y < 0. ) or ( x < 0. & y <= 0. ) ) by A1;

suppose ( x <= 0. & y < 0. ) ; :: thesis: ( ( a <= 0 & b < 0 ) or ( a < 0 & b <= 0 ) )

hence ( ( a <= 0 & b < 0 ) or ( a < 0 & b <= 0 ) ) ; :: thesis: verum

end;

suppose ( x < 0. & y <= 0. ) ; :: thesis: ( ( a <= 0 & b < 0 ) or ( a < 0 & b <= 0 ) )

hence ( ( a <= 0 & b < 0 ) or ( a < 0 & b <= 0 ) ) ; :: thesis: verum

end;

end;

end;

hence ( ( a <= 0 & b < 0 ) or ( a < 0 & b <= 0 ) ) ; :: thesis: verum

end;

then a + b < 0 + 0 ;
hence x + y < 0. by SUPINF_2:1; :: thesis: verum

end;

end;

end;

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

end;

end;