let A, B be ext-real-membered set ; :: thesis: inf (A \/ B) = min ((inf A),(inf B))
set m = min ((inf A),(inf B));
A1: inf B is LowerBound of B by Def4;
A2: 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 B by Th5, XBOOLE_1:7;
then A3: x <= inf B by Def4;
x is LowerBound of A by Th5, XBOOLE_1:7;
then x <= inf A by Def4;
hence x <= min ((inf A),(inf B)) by A3, XXREAL_0:20; :: thesis: verum
end;
inf A is LowerBound of A by Def4;
then min ((inf A),(inf B)) is LowerBound of A \/ B by A1, Th7;
hence inf (A \/ B) = min ((inf A),(inf B)) by A2, Def4; :: thesis: verum