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