let X, Y be non empty Subset of ExtREAL ; :: thesis: sup (X + Y) <= (sup X) + (sup Y)
for z being ext-real number st z in X + Y holds
z <= (sup X) + (sup Y)

proof

let z be ext-real number ; :: 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: x in X and
A2: y in Y and
A3: z = x + y by Def5;
A4: y <= sup Y by A2, XXREAL_2:4;
x <= sup X by A1, XXREAL_2:4;
hence z <= (sup X) + (sup Y) by A3, A4, XXREAL_3:38; :: 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