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

proof

now

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

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

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

end;

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

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

end;

end;

end;

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

end;

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

end;

end;

end;

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

end;

end;