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)

hence sup (X + Y) <= (sup X) + (sup Y) by XXREAL_2:def 3; :: thesis: verum

for z being ExtReal st z in X + Y holds

z <= (sup X) + (sup Y)

proof

then
(sup X) + (sup Y) is UpperBound of X + Y
by XXREAL_2:def 1;
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;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

hence sup (X + Y) <= (sup X) + (sup Y) by XXREAL_2:def 3; :: thesis: verum