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
A2: ( x in X & y in Y & z = x + y ) by Def5;
( x <= sup X & y <= sup Y ) by A2, XXREAL_2:4;
hence z <= (sup X) + (sup Y) by A2, 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