let X, Y be non empty Subset of ExtREAL; :: thesis: (inf X) + (inf Y) <= inf (X + Y)
for z being ExtReal st z in X + Y holds
(inf X) + (inf Y) <= z

proof

let z be ExtReal; :: thesis: ( z in X + Y implies (inf X) + (inf Y) <= z )
assume z in X + Y ; :: thesis: (inf X) + (inf Y) <= z
then consider x, y being R_eal such that
A1: z = x + y and
A2: x in X and
A3: y in Y ;
A4: inf Y <= y by A3, XXREAL_2:3;
inf X <= x by A2, XXREAL_2:3;
hence (inf X) + (inf Y) <= z by A1, A4, XXREAL_3:36; :: thesis: verum

end;

then (inf X) + (inf Y) is LowerBound of X + Y by XXREAL_2:def 2;
hence (inf X) + (inf Y) <= inf (X + Y) by XXREAL_2:def 4; :: thesis: verum