let A, B be ext-real-membered set ; :: thesis: inf (A \/ B) = min (inf A),(inf B)
set m = min (inf A),(inf B);
B: inf A is LowerBound of A by Def4;
inf B is LowerBound of B by Def4;
then A: min (inf A),(inf B) is LowerBound of A \/ B by B, Th5;
for x being LowerBound of A \/ B holds x <= min (inf A),(inf B)

proof

let x be LowerBound of A \/ B; :: thesis: x <= min (inf A),(inf B)
x is LowerBound of A by Th4, XBOOLE_1:7;
then C: x <= inf A by Def4;
x is LowerBound of B by Th4, XBOOLE_1:7;
then x <= inf B by Def4;
hence x <= min (inf A),(inf B) by C, XXREAL_0:20; :: thesis: verum

end;

hence inf (A \/ B) = min (inf A),(inf B) by A, Def4; :: thesis: verum