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, Th70;
hence max (inf X),(inf Y) <= inf (X /\ Y) by Def4; :: thesis: verum