let X, Y be non empty Subset of ExtREAL; :: thesis: sup (X + Y) <= (sup X) + (sup Y)
for z being ExtReal st z in X + Y holds
z <= (sup X) + (sup Y)
proof
let z be ExtReal; :: thesis: ( z in X + Y implies z <= (sup X) + (sup Y) )
assume z in X + Y ; :: thesis: z <= (sup X) + (sup Y)
then consider x, y being R_eal such that
A1: z = x + y and
A2: x in X and
A3: y in Y ;
A4: y <= sup Y by A3, XXREAL_2:4;
x <= sup X by A2, XXREAL_2:4;
hence z <= (sup X) + (sup Y) by A1, A4, XXREAL_3:36; :: thesis: verum
end;
then (sup X) + (sup Y) is UpperBound of X + Y by XXREAL_2:def 1;
hence sup (X + Y) <= (sup X) + (sup Y) by XXREAL_2:def 3; :: thesis: verum