let X, Y be ext-real-membered set ; :: thesis: max ((inf X),(inf Y)) <= inf (X /\ Y)
A1: inf Y is LowerBound of Y by Def4;
inf X is LowerBound of X by Def4;
then max ((inf X),(inf Y)) is LowerBound of X /\ Y by A1, Th66;
hence max ((inf X),(inf Y)) <= inf (X /\ Y) by Def4; :: thesis: verum