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

proof

let z be ext-real number ; :: 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
A2: ( x in X & y in Y & z = x + y ) by Def5;
( inf X <= x & inf Y <= y ) by A2, XXREAL_2:3;
hence (inf X) + (inf Y) <= z by A2, XXREAL_3:38; :: 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