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