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))

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

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

inf A is LowerBound of A
by Def4;
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;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

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