let X, Y be ext-real-membered set ; :: thesis: inf (X \/ Y) = min (inf X),(inf Y)
set a = inf (X \/ Y);
A1: inf Y is LowerBound of Y by Def4;
inf X is LowerBound of X by Def4;
then min (inf X),(inf Y) is LowerBound of X \/ Y by A1, Th66;
then A2: min (inf X),(inf Y) <= inf (X \/ Y) by Def4;
A3: inf (X \/ Y) <= inf Y by Th60, XBOOLE_1:7;
inf (X \/ Y) <= inf X by Th60, XBOOLE_1:7;
then inf (X \/ Y) <= min (inf X),(inf Y) by A3, XXREAL_0:20;
hence inf (X \/ Y) = min (inf X),(inf Y) by A2, XXREAL_0:1; :: thesis: verum