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

hence (inf X) + (inf Y) <= inf (X + Y) by XXREAL_2:def 4; :: thesis: verum

for z being ExtReal st z in X + Y holds

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

proof

then
(inf X) + (inf Y) is LowerBound of X + Y
by XXREAL_2:def 2;
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;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

hence (inf X) + (inf Y) <= inf (X + Y) by XXREAL_2:def 4; :: thesis: verum